Derivative limit theorem - #2032

Open

nmolinamounier wants to merge 16 commits into

math-comp:masterfrom

nmolinamounier:deriv_limit_thm

Commits on Jul 15, 2026

Move `is_deriveV` and `is_derive1_comp` to `derive.v`
nmolinamounier
committed
8f34028
Utility lemmas in filter.v
nmolinamounier
committed
b2536f8
New derive lemmas
nmolinamounier
committed
bfe3f74
Update changelog
nmolinamounier
committed
96d6680
Fix indentation
nmolinamounier
committed
f11fbda
Add dependency on #2029 for CI
nmolinamounier
committed
8e9b802
Topology lemmas
nmolinamounier
committed
022fed0
normed module neighborhood lemmas
nmolinamounier
committed
fa30e1f
Update changelog
nmolinamounier
committed
cbb96a1
Add dependency on #2027 for CI
nmolinamounier
committed
553bc3a
Correct dependency to #2024
nmolinamounier
committed
49b25e0
Derivative limit theorem
nmolinamounier
committed
38aa6a9
Update changelog
nmolinamounier
committed
49eeb57
Missing `num_topology` lemmas
nmolinamounier
committed
db98ac7
Add dependency on #2030 for CI
nmolinamounier
committed
4f54daa
fix lemma name
nmolinamounier
committed
f6585bc