Commit 2025-10-30 08:31 aab64f2d

View on Github →

chore(Analysis/Distribution): fix name of a theorem (#31073) As pointed out by @ADedecker the name should not contain the _aux suffix.

Estimated changes

Modified Mathlib/Analysis/Distribution/SchwartzSpace.lean

Modified Mathlib/Analysis/Distribution/TemperateGrowth.lean

added theorem Function.HasTemperateGrowth.norm_iteratedFDeriv_le_uniform

deleted theorem Function.HasTemperateGrowth.norm_iteratedFDeriv_le_uniform_aux