List view

fixes #1123 (unusable lemma)

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

Status: Merged (completed).

math-comp/analysisnumber 1124

#1124 In math-comp/analysis;

· by affeldt-aist was closed on Dec 26, 2023

fixes #667

Status: Merged (completed).

math-comp/analysisnumber 1127

#1127 In math-comp/analysis;

· by affeldt-aist was closed on Dec 27, 2023

rm dup lemmas

Status: Merged (completed).

math-comp/analysisnumber 1129

#1129 In math-comp/analysis;

· by affeldt-aist was closed on Jan 1, 2024

helper lemmas for contra (PR #1119)

Status: Merged (completed).

math-comp/analysisnumber 1136

#1136 In math-comp/analysis;

· by Tragicus was closed on Jan 8, 2024

format doc

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 1130

#1130 In math-comp/analysis;

· by affeldt-aist was closed on Jan 7, 2024

change contra_not when requiring MathComp > 1.14

Status: Closed (completed).

#667 In math-comp/analysis;

· by affeldt-aist was closed on Dec 27, 2023

coqdoc formatting command

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

Status: Closed (completed).

#1071 In math-comp/analysis;

· by affeldt-aist was closed on Jan 8, 2024

Alternative definition of Chernoff

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

#1078 In math-comp/analysis;

· by hoheinzollern was closed on Jan 8, 2024

Add cantor.v to theories/Make

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

Status: Closed (completed).

#1098 In math-comp/analysis;

· by affeldt-aist was closed on Nov 17, 2023

Is cantor_pseudoMetric necessary?

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

Status: Closed (completed).

#1099 In math-comp/analysis;

· by affeldt-aist was closed on Nov 17, 2023

move ae_eq?

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

Status: Closed (completed).

#1096 In math-comp/analysis;

· by IshiguroYoshihiro was closed on Dec 21, 2023

lnX -> lnXn

Status: Closed (completed).

#1093 In math-comp/analysis;

· by hoheinzollern was closed on Nov 17, 2023

non-informative comment

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

Status: Closed (completed).

#1104 In math-comp/analysis;

· by affeldt-aist was closed on Nov 17, 2023

lacks a Proof command

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

Status: Closed (completed).

#1103 In math-comp/analysis;

· by affeldt-aist was closed on Nov 17, 2023

Lacking a Proof command

Status: Closed (completed).

#1114 In math-comp/analysis;

· by affeldt-aist was closed on Jan 8, 2024

unsusable lemma

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

Status: Closed (completed).

#1123 In math-comp/analysis;

· by affeldt-aist was closed on Dec 26, 2023