List view

Broken in Coq CI

"bug" 🐛This issue (resp. PR) describes (resp. fixes) a "bug"This issue (resp. PR) describes (resp. fixes) a "bug"

Status: Closed (completed).

#1333 In math-comp/analysis;

· by SkySkimmer was closed on Oct 2, 2024

move Require Import to top of the file

Status: Closed (completed).

#1334 In math-comp/analysis;

· by affeldt-aist was closed on Oct 8, 2024

duplicate line

"bug" 🐛This issue (resp. PR) describes (resp. fixes) a "bug"This issue (resp. PR) describes (resp. fixes) a "bug"

Status: Closed (completed).

#1343 In math-comp/analysis;

· by affeldt-aist was closed on Oct 8, 2024

\oo should be documented in filter.v

documentation 📝This issue/PR is about documentation of the library / repositoryThis issue/PR is about documentation of the library / repository

Status: Closed (completed).

#1342 In math-comp/analysis;

· by affeldt-aist was closed on Oct 8, 2024

maxeMr: can be generalized to large inequality

enhancement ✨This issue/PR is about adding new features enhancing the libraryThis issue/PR is about adding new features enhancing the library

Status: Closed (completed).

#1329 In math-comp/analysis;

· by affeldt-aist was closed on Oct 1, 2024