Search results

measure_function.isFinite override fintype.isFinite

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

Status: Open.

#1943 In math-comp/analysis;

· CohenCyril opened on Apr 21, 2026

·  

1.17.0

fix documentation in set_interval.v

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

Status: Open.

#1942 In math-comp/analysis;

· affeldt-aist opened on Apr 19, 2026

·  

1.17.0

Make pseudometric_normedZmodType depend on topologicalNmodule

Status: Open.

#1935 In math-comp/analysis;

· mkerjean opened on Apr 15, 2026

·  

1.18.0

continuous_linear_bounded should be generalized to convexTvsType

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

Status: Open.

#1927 In math-comp/analysis;

· affeldt-aist opened on Apr 3, 2026

·  

1.17.0

rename to continuous_fun?

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

Status: Open.

#1926 In math-comp/analysis;

· affeldt-aist opened on Apr 3, 2026

·  

1.17.0

rename sub_sigma_algebra2

Status: Open.

#1923 In math-comp/analysis;

· affeldt-aist opened on Mar 31, 2026

·  

1.17.0

consider making the information r > 0 explicit in open_subball_rat?

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

Status: Open.

#1920 In math-comp/analysis;

· affeldt-aist opened on Mar 26, 2026

·  

1.17.0

Vector space with basis

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

Status: Open.

#1911 In math-comp/analysis;

· Tragicus opened on Mar 19, 2026

·  

1.17.0

packager: coq -> rocq

packaging/releasingIssue/PR about packaging or realising.Issue/PR about packaging or realising.

Status: Open.

#1905 In math-comp/analysis;

· affeldt-aist opened on Mar 16, 2026

·  

1.17.0

funrpos and funepos should be factorized

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

wish 🙏Request for a specific mathematical resultRequest for a specific mathematical result

Status: Open.

#1903 In math-comp/analysis;

· affeldt-aist opened on Mar 15, 2026

·  

1.17.0

is_derive instances for max function

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

Status: Open.

#1898 In math-comp/analysis;

· affeldt-aist opened on Mar 12, 2026

·  

1.17.0

about the notation f \max g

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

Status: Open.

#1897 In math-comp/analysis;

· affeldt-aist opened on Mar 12, 2026

·  

1.17.0