Commit 2025-10-30 12:48 781c8d95

View on Github →

chore(Analysis/Distribution/TemperateGrowth): avoid redefining variables (#31075) Pointed out by @ADedecker in a previous PR. Also rename D to E to have consistent names for the variables in this file. Now all generic maps are from E to F.

Estimated changes

Modified Mathlib/Analysis/Distribution/TemperateGrowth.lean

modified def MeasureTheory.Measure.integrablePower

modified theorem integrable_of_le_of_pow_mul_le