Commit 2025-03-31 07:29 c9db85e2

View on Github →

feat(Analysis/Asymptotics): generalize asymptotics results to NormMulClass (#23347) This generalizes many results on asymptotics currently proved for a NormedDivisionRing using the new NormMulClass typeclass.

Estimated changes

Modified Mathlib/Analysis/Asymptotics/Defs.lean

modified theorem Asymptotics.IsBigO.const_mul_right

modified theorem Asymptotics.IsBigO.mul

modified theorem Asymptotics.IsBigO.mul_isLittleO

modified theorem Asymptotics.IsBigO.pow

modified theorem Asymptotics.IsBigOWith.const_mul_right

modified theorem Asymptotics.IsBigOWith.mul

modified theorem Asymptotics.IsBigOWith.of_pow

modified theorem Asymptotics.IsBigOWith.pow'

modified theorem Asymptotics.IsBigOWith.pow

modified theorem Asymptotics.IsLittleO.const_mul_right

modified theorem Asymptotics.IsLittleO.mul

modified theorem Asymptotics.IsLittleO.mul_isBigO

modified theorem Asymptotics.IsLittleO.of_pow

modified theorem Asymptotics.IsLittleO.pow

modified theorem Asymptotics.isBigOWith_self_const_mul

modified theorem Asymptotics.isBigO_const_mul_left_iff

modified theorem Asymptotics.isBigO_const_mul_right_iff

modified theorem Asymptotics.isBigO_self_const_mul

modified theorem Asymptotics.isLittleO_const_mul_left_iff

modified theorem Asymptotics.isLittleO_const_mul_right_iff

Modified Mathlib/Analysis/SpecialFunctions/Pow/Asymptotics.lean