Mathlib Changelog
v4
Changelog
About
Github
Commit
2025-11-05 05:40
02e01097
View on Github →
feat(Analysis/Distribution): basic algebraic properties of functions of temperate growth (
#31112
)
Estimated changes
Modified
Mathlib/Analysis/Asymptotics/Lemmas.lean
added
theorem
Asymptotics.IsBigO.pow_of_le_right
Modified
Mathlib/Analysis/Calculus/ContDiff/Operations.lean
added
theorem
iteratedFDeriv_add
added
theorem
iteratedFDeriv_neg
Modified
Mathlib/Analysis/Distribution/TemperateGrowth.lean
added
theorem
Function.HasTemperateGrowth.add
added
theorem
Function.HasTemperateGrowth.neg
added
theorem
Function.HasTemperateGrowth.sub