List view

gee_pmull: hypo 0 < x can be slightly generalized

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).

#1203 In math-comp/analysis;

· by affeldt-aist was closed on Apr 2, 2024

typo

renaming/refactoring 🔧This is about a renaming or refactoring in the libraryThis is about a renaming or refactoring in the library

Status: Closed (completed).

#1208 In math-comp/analysis;

· by affeldt-aist was closed on Apr 19, 2024

spurious integrability condition

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

Status: Closed (completed).

#1212 In math-comp/analysis;

· by affeldt-aist was closed on Apr 18, 2024

inf_lower_bound and inf_lb

renaming/refactoring 🔧This is about a renaming or refactoring in the libraryThis is about a renaming or refactoring in the library

Status: Closed (completed).

#1226 In math-comp/analysis;

· by affeldt-aist was closed on Jun 5, 2024

rename the misc subdir to showcase

renaming/refactoring 🔧This is about a renaming or refactoring in the libraryThis is about a renaming or refactoring in the library

Status: Closed (completed).

#1233 In math-comp/analysis;

· by affeldt-aist was closed on Jun 3, 2024

naming

renaming/refactoring 🔧This is about a renaming or refactoring in the libraryThis is about a renaming or refactoring in the library

Status: Closed (completed).

#1229 In math-comp/analysis;

· by affeldt-aist was closed on Jun 3, 2024

small generalization of Markov's lemma

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).

#1232 In math-comp/analysis;

· by affeldt-aist was closed on Jun 3, 2024

dead code in realfun.v

Status: Closed (completed).

#1237 In math-comp/analysis;

· by affeldt-aist was closed on Jun 5, 2024

typo in functions.v's doc

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

Status: Closed (completed).

#1236 In math-comp/analysis;

· by affeldt-aist was closed on Jun 5, 2024

Naming of sigma subadditivity

Status: Closed (completed).

#981 In math-comp/analysis;

· by affeldt-aist was closed on Apr 2, 2024

integrableM lemmas

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

Status: Merged (completed).

math-comp/analysisnumber 1207

#1207 In math-comp/analysis;

· by affeldt-aist was closed on Apr 11, 2024

not_near_at_leftP

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

Status: Merged (completed).

math-comp/analysisnumber 1221

#1221 In math-comp/analysis;

· by IshiguroYoshihiro was closed on May 14, 2024

Adapt to math-comp/math-comp#1166

Status: Merged (completed).

math-comp/analysisnumber 1189

#1189 In math-comp/analysis;

· by pi8027 was closed on Apr 19, 2024