lemmas around exponential growth - #2036

Open

amolinamounier wants to merge 21 commits into

math-comp:masterfrom

amolinamounier:exp_growth

Commits on Jul 15, 2026

Move `is_deriveV` and `is_derive1_comp` to `derive.v`
amolinamounier
committed
8f34028
Utility lemmas in filter.v
amolinamounier
committed
b2536f8
New derive lemmas
amolinamounier
committed
bfe3f74
Update changelog
amolinamounier
committed
96d6680
Fix indentation
amolinamounier
committed
f11fbda
normed module identity convergence lemmas
amolinamounier
committed
75a0948
Update changelog
amolinamounier
committed
7607dd5
Add dependency on #2029 for CI
amolinamounier
committed
8e9b802
Topology lemmas
amolinamounier
committed
022fed0
normed module neighborhood lemmas
amolinamounier
committed
fa30e1f
Update changelog
amolinamounier
committed
cbb96a1
Add dependency on #2027 for CI
amolinamounier
committed
553bc3a
Correct dependency to #2024
amolinamounier
committed
49b25e0
Missing `num_topology` lemmas
amolinamounier
committed
db98ac7
L'Hôpital's rule for infty/infty forms
amolinamounier
committed
3862db4
Update changelog
amolinamounier
committed
efaa663
Merge branch 'normed_nbhs_lemmas' into exp_growth
amolinamounier
committed
2f3362e
Merge branch 'identity_cvg_lemmas' into exp_growth
amolinamounier
committed
8c4a59c
exponential growth lemmas
amolinamounier
committed
883e6b7
Add dependency on #2029 for CI
amolinamounier
committed
9fc7041
Add dependency on #2034 for CI
amolinamounier
committed
9ba7af3