List view

should be maxe_pMr

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

Status: Closed (completed).

#1389 In math-comp/analysis;

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

rename to preimage_itv_cy ?

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

Status: Closed (completed).

#1390 In math-comp/analysis;

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

too specific lemma

Status: Closed (completed).

#1408 In math-comp/analysis;

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

two files named path.v

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

Status: Closed (completed).

#1412 In math-comp/analysis;

· by affeldt-aist was closed on Dec 4, 2024

Path conflict on theories/homotopy_theory/path.v with core ssreflect path.v

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

Status: Closed (completed).

#1425 In math-comp/analysis;

· by MSoegtropIMC was closed on Dec 4, 2024

prod notation for ereal and 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 1418

#1418 In math-comp/analysis;

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

instances for measures

Status: Merged (completed).

math-comp/analysisnumber 1419

#1419 In math-comp/analysis;

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