Commit 2024-02-14 09:39 1c8f2465

View on Github →

feat(Analysis/Asymptotics/Asymptotics): generalize smul lemmas to normed rings (#9811) Using BoundedSMul instead of NormedSpace makes these true more generally. The old proofs do not generalize, so are replaced with copies of the mul proofs. The const_smul_self lemmas match the existing const_mul_self ones. shake then reports that the imports can be reduced.

Estimated changes

Modified Mathlib/Analysis/Asymptotics/Asymptotics.lean

modified theorem Asymptotics.IsBigO.const_smul_left

added theorem Asymptotics.IsBigO.const_smul_self

modified theorem Asymptotics.IsBigOWith.const_smul_left

added theorem Asymptotics.IsBigOWith.const_smul_self

modified theorem Asymptotics.IsLittleO.const_smul_left

modified theorem Asymptotics.IsLittleO.tendsto_inv_smul_nhds_zero

modified theorem Asymptotics.isBigOWith_of_eq_mul

Modified Mathlib/Analysis/Asymptotics/SpecificAsymptotics.lean

Modified Mathlib/Analysis/Asymptotics/Theta.lean

Modified Mathlib/Analysis/SpecificLimits/Normed.lean

Modified Mathlib/Order/Filter/ZeroAndBoundedAtFilter.lean