Commit 2026-01-12 13:34 cc13e767

View on Github →

chore(Asymptotics/Lemmas): weaken Normed -> Seminormed (#33869)

Estimated changes

Modified Mathlib/Analysis/Asymptotics/Lemmas.lean

modified theorem Asymptotics.IsLittleO.tendsto_zero_of_tendsto

modified theorem Asymptotics.isBigOWith_pi

modified theorem Asymptotics.isBigO_pi

modified theorem Asymptotics.isLittleO_pi

modified theorem NormedField.tendsto_zero_smul_of_tendsto_zero_of_bounded