List view

fixes #1735 (adjacent_seq)

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 1745

#1745 In math-comp/analysis;

· by affeldt-aist was closed on Oct 31, 2025

generalize onem

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 1737

#1737 In math-comp/analysis;

· by affeldt-aist was closed on Oct 23, 2025

more dir locals for company-coq

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 1724

#1724 In math-comp/analysis;

· by affeldt-aist was closed on Nov 7, 2025

beta distribution

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 1640

#1640 In math-comp/analysis;

· by affeldt-aist was closed on Nov 7, 2025

Closed ball0 20250911

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 1717

#1717 In math-comp/analysis;

· by affeldt-aist was closed on Sep 16, 2025

littleoE0

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 1707

#1707 In math-comp/analysis;

· by Tragicus was closed on Sep 16, 2025

CI: 📝 👷 make html generate hierarchy graph

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

Status: Merged (completed).

math-comp/analysisnumber 1710

#1710 In math-comp/analysis;

· by yoshihiro503 was closed on Sep 18, 2025

add lemma lt0_adde

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 1715

#1715 In math-comp/analysis;

· by affeldt-aist was closed on Sep 18, 2025

Fixes 1729

Status: Merged (completed).

math-comp/analysisnumber 1732

#1732 In math-comp/analysis;

· by affeldt-aist was closed on Oct 7, 2025

add measure theory to dependency graph

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

Status: Merged (completed).

math-comp/analysisnumber 1728

#1728 In math-comp/analysis;

· by affeldt-aist was closed on Nov 5, 2025

fixes #1733 (ln_eq0)

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 1744

#1744 In math-comp/analysis;

· by affeldt-aist was closed on Nov 6, 2025

fixes #1734 (renaming derivable_oo_continuous_bnd)

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 1747

#1747 In math-comp/analysis;

· by affeldt-aist was closed on Nov 6, 2025

continuous_big

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 1706

#1706 In math-comp/analysis;

· by Tragicus was closed on Sep 11, 2025

add lemma cvg_addrl_Ny

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 1716

#1716 In math-comp/analysis;

· by affeldt-aist was closed on Sep 11, 2025

add lemmas for derivable_oo/Nyo/oy_continuous_bnd

Status: Merged (completed).

math-comp/analysisnumber 1656

#1656 In math-comp/analysis;

· by IshiguroYoshihiro was closed on Oct 9, 2025

Make cdf an instance of Cumulative (fix #1572)

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 1686

#1686 In math-comp/analysis;

· by Yosuke-Ito-345 was closed on Aug 23, 2025

missing near lemma

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 1699

#1699 In math-comp/analysis;

· by affeldt-aist was closed on Aug 23, 2025

fixes #1627

build/continuous integration ⚙️This issue/PR is about the build process or CIThis issue/PR is about the build process or CI

Status: Merged (completed).

math-comp/analysisnumber 1725

#1725 In math-comp/analysis;

· by affeldt-aist was closed on Sep 24, 2025

split measure.v

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 1719

#1719 In math-comp/analysis;

· by affeldt-aist was closed on Sep 24, 2025

Lemma measure_addE requires extra parameter

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

Status: Closed (completed).

#1077 In math-comp/analysis;

· by hoheinzollern was closed on Sep 5, 2025

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

#1552 In math-comp/analysis;

· by affeldt-aist was closed on Sep 24, 2025

wrong levels in the notations for expectation and variance

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

Status: Closed (completed).

#1722 In math-comp/analysis;

· by affeldt-aist was closed on Sep 24, 2025

More robust command in Makefile.common to generate the documentation

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

Status: Closed (completed).

#1702 In math-comp/analysis;

· by affeldt-aist was closed on Sep 18, 2025

num_normedtype.v imported HB but doesn't use

build/continuous integration ⚙️This issue/PR is about the build process or CIThis issue/PR is about the build process or CI

Status: Closed (completed).

#1627 In math-comp/analysis;

· by IshiguroYoshihiro was closed on Sep 24, 2025

hypothesis can be weakened

Status: Closed (completed).

#1727 In math-comp/analysis;

· by affeldt-aist was closed on Oct 7, 2025