List view

is_derive1_sqrt 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 1679

#1679 In math-comp/analysis;

· by yosakaon was closed on Jul 7, 2025

extract a last few lemmas from the sampling branch

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 1678

#1678 In math-comp/analysis;

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

Remove some unnecessary use of unitfE

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 1571

#1571 In math-comp/analysis;

· by pi8027 was closed on Jul 3, 2025

rm forms.v

Status: Merged (completed).

math-comp/analysisnumber 1673

#1673 In math-comp/analysis;

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

fixes #1687

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

experiment 🧪This issue/PR is very experimentalThis issue/PR is very experimental

Status: Merged (completed).

math-comp/analysisnumber 1688

#1688 In math-comp/analysis;

· by affeldt-aist was closed on Jul 21, 2025

fix #1336

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 1693

#1693 In math-comp/analysis;

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

generalized measurable_fun_itv_(bndo_bndc/obnd_cbnd)

Status: Merged (completed).

math-comp/analysisnumber 1662

#1662 In math-comp/analysis;

· by IshiguroYoshihiro was closed on Aug 13, 2025

fixes #1647

Status: Merged (completed).

math-comp/analysisnumber 1696

#1696 In math-comp/analysis;

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

simplify lemma lebesgue_measure_rat

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 1700

#1700 In math-comp/analysis;

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

fixes #1551 (move <code>isMeasurable</code> from <code>simple_functions.v</code> to <code>measure.v</code>)

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 1695

#1695 In math-comp/analysis;

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

Missing theory for Hoelder conjugates

Status: Closed (completed).

#1075 In math-comp/analysis;

· by hoheinzollern was closed on Jul 8, 2025

measurable_sfunP does not refer to sfun

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

Status: Closed (completed).

#1518 In math-comp/analysis;

· by t6s was closed on Aug 16, 2025

<code>isMeasurableFun</code> should live in <code>measure.v</code>

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

Status: Closed (completed).

#1551 In math-comp/analysis;

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

MathComp-Analysis 1.12.0 requires at least HB 1.8.0

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

#1687 In math-comp/analysis;

· by affeldt-aist was closed on Jul 21, 2025

'derivemxE' new name proposal

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

Status: Closed (completed).

#1647 In math-comp/analysis;

· by yosakaon was closed on Aug 13, 2025