proof of L'Hopital rule#1371

Closed

ndslusarz wants to merge 15 commits intomath-comp:masterfrom

ndslusarz:lhopital

Commits on Feb 12, 2025

minor generalization

affeldt-aist
authored and
ndslusarz
committed
simplifications

CohenCyril
authored and
ndslusarz
committed
add lemma measurable_powRr

affeldt-aist
authored and
ndslusarz
committed
factorize code about powerset sigma-algebras

affeldt-aist
authored and
ndslusarz
committed
changelog for 1.8.0 (#1439)

authored and
ndslusarz
committed
initial commit

LaurenceRideau
authored and
ndslusarz
committed
complete Niven's proof

affeldt-aist
authored and
ndslusarz
committed
lock funepos and funeneg

Tragicus
authored and
ndslusarz
committed
perf patch lebesgue_integral.v (#1441)

Tragicus
authored and
ndslusarz
committed
minor generalization and renaming (#1443)

affeldt-aist
authored and
ndslusarz
committed
generalize indexing in lemmas for series (#1397)

authored and
ndslusarz
committed
Import ZArith to use it in Rstruct.v

andres-erbsen
authored and
ndslusarz
committed
lhopital + cauchy mvt
ndslusarz
committed
deduplicating into lemma
ndslusarz
committed
mv lemmas to derive

affeldt-aist
authored and
ndslusarz
committed