lemmas around exponential growth - #2036

Open

nmolinamounier wants to merge 21 commits into

math-comp:masterfrom

nmolinamounier:exp_growth

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
normed module identity convergence lemmas
nmolinamounier
committed
75a0948
Update changelog
nmolinamounier
committed
7607dd5
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
Missing `num_topology` lemmas
nmolinamounier
committed
db98ac7
L'Hôpital's rule for infty/infty forms
nmolinamounier
committed
3862db4
Update changelog
nmolinamounier
committed
efaa663
Merge branch 'normed_nbhs_lemmas' into exp_growth
nmolinamounier
committed
2f3362e
Merge branch 'identity_cvg_lemmas' into exp_growth
nmolinamounier
committed
8c4a59c
exponential growth lemmas
nmolinamounier
committed
883e6b7
Add dependency on #2029 for CI
nmolinamounier
committed
9fc7041
Add dependency on #2034 for CI
nmolinamounier
committed
9ba7af3