List view

rm dep on topo and ereal from altreals

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

Status: Merged (completed).

math-comp/analysisnumber 1353

#1353 In math-comp/analysis;

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

fixes #1345

Status: Merged (completed).

math-comp/analysisnumber 1363

#1363 In math-comp/analysis;

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

Rintegral atan expR

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 1356

#1356 In math-comp/analysis;

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

Bounded and landau notations

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

question ❓There is an unanswered question hereThere is an unanswered question here

Status: Closed (completed).

#271 In math-comp/analysis;

· by mkerjean was closed on Oct 11, 2024

Relation composition

Status: Closed (completed).

#759 In math-comp/analysis;

· by zstone1 was closed on Oct 11, 2024

Splitting topology.v

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

Status: Closed (completed).

#1167 In math-comp/analysis;

· by zstone1 was closed on Oct 23, 2024

useless type constraint

Status: Closed (completed).

#1357 In math-comp/analysis;

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

depency of altreals on topology and ereal not needed

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

Status: Closed (completed).

#1352 In math-comp/analysis;

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

shouldn't this equivalence with suffixed with P?

question ❓There is an unanswered question hereThere is an unanswered question here

Status: Closed (completed).

#1345 In math-comp/analysis;

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