-
Notifications
You must be signed in to change notification settings - Fork 73
OpenAug 23, 2026
Due by August 31, 2026
•Last updated 21% complete
List view
0 of 75 selected 0 issues of 75 selected
- Status: Open.#1935 In math-comp/analysis;
Split
probability.vinto a directoryprobability_theoryrenaming/refactoring 🔧This is about a renaming or refactoring in the libraryThis is about a renaming or refactoring in the libraryStatus: Open.#1808 In math-comp/analysis;finitely-supported probability measure
wish 🙏Request for a specific mathematical resultRequest for a specific mathematical resultStatus: Open.#1227 In math-comp/analysis;generalize
Order_isNbhsenhancement ✨This issue/PR is about adding new features enhancing the libraryThis issue/PR is about adding new features enhancing the libraryStatus: Open.#1779 In math-comp/analysis;move to
classical_sets.venhancement ✨This issue/PR is about adding new features enhancing the libraryThis issue/PR is about adding new features enhancing the libraryStatus: Open.#1967 In math-comp/analysis;TODO: rename
pseudometricrenaming/refactoring 🔧This is about a renaming or refactoring in the libraryThis is about a renaming or refactoring in the libraryStatus: Open.#1990 In math-comp/analysis;- Status: Open.#1994 In math-comp/analysis;
notation for intervals
"bug" 🐛This issue (resp. PR) describes (resp. fixes) a "bug"This issue (resp. PR) describes (resp. fixes) a "bug"enhancement ✨This issue/PR is about adding new features enhancing the libraryThis issue/PR is about adding new features enhancing the libraryStatus: Open.#795 In math-comp/analysis;- Status: Open.#1401 In math-comp/analysis;
CPOs (wip)
experiment 🧪This issue/PR is very experimentalThis issue/PR is very experimentalStatus: Draft (not ready).shorten proof about monotonic functions
enhancement ✨This issue/PR is about adding new features enhancing the libraryThis issue/PR is about adding new features enhancing the libraryStatus: Open.#1156 In math-comp/analysis;Sorgenfrey line
wish 🙏Request for a specific mathematical resultRequest for a specific mathematical resultStatus: Open.#1044 In math-comp/analysis;move the product measure out of
lebesgue_integral_fubini.vrenaming/refactoring 🔧This is about a renaming or refactoring in the libraryThis is about a renaming or refactoring in the libraryStatus: Open.#1554 In math-comp/analysis;conv_gt0as an instance ofPosNumenhancement ✨This issue/PR is about adding new features enhancing the libraryThis issue/PR is about adding new features enhancing the libraryStatus: Open.#1009 In math-comp/analysis;Have notations for deriving and derivability
documentation 📝This issue/PR is about documentation of the library / repositoryThis issue/PR is about documentation of the library / repositoryenhancement ✨This issue/PR is about adding new features enhancing the libraryThis issue/PR is about adding new features enhancing the libraryquestion ❓There is an unanswered question hereThere is an unanswered question hererenaming/refactoring 🔧This is about a renaming or refactoring in the libraryThis is about a renaming or refactoring in the libraryStatus: Open.#68 In math-comp/analysis;Remove
bigmaxrfromRstruct.v?renaming/refactoring 🔧This is about a renaming or refactoring in the libraryThis is about a renaming or refactoring in the libraryStatus: Open.#1739 In math-comp/analysis;Near message error
enhancement ✨This issue/PR is about adding new features enhancing the libraryThis issue/PR is about adding new features enhancing the libraryquestion ❓There is an unanswered question hereThere is an unanswered question hereStatus: Open.#1320 In math-comp/analysis;improve the interface for the product measure
wish 🙏Request for a specific mathematical resultRequest for a specific mathematical resultStatus: Open.#1665 In math-comp/analysis;near notation inference issues
"bug" 🐛This issue (resp. PR) describes (resp. fixes) a "bug"This issue (resp. PR) describes (resp. fixes) a "bug"Status: Open.#548 In math-comp/analysis;Near Notation can't solve
g \is_near F"bug" 🐛This issue (resp. PR) describes (resp. fixes) a "bug"This issue (resp. PR) describes (resp. fixes) a "bug"Status: Open.#549 In math-comp/analysis;potential generalization from
realDomainTypetonumDomainTypeenhancement ✨This issue/PR is about adding new features enhancing the libraryThis issue/PR is about adding new features enhancing the libraryStatus: Open.#696 In math-comp/analysis;Lnorm0enhancement ✨This issue/PR is about adding new features enhancing the libraryThis issue/PR is about adding new features enhancing the libraryexperiment 🧪This issue/PR is very experimentalThis issue/PR is very experimentalStatus: Open.#1643 In math-comp/analysis;variant of
measurable_fun_eqrwish 🙏Request for a specific mathematical resultRequest for a specific mathematical resultStatus: Open.#1319 In math-comp/analysis;Generalize integration_by_parts
enhancement ✨This issue/PR is about adding new features enhancing the libraryThis issue/PR is about adding new features enhancing the libraryStatus: Open (in progress).Could we have a nix upgrade documentation somewhere? (@amahboubi)
documentation 📝This issue/PR is about documentation of the library / repositoryThis issue/PR is about documentation of the library / repositoryStatus: Open.#151 In math-comp/analysis;