Commit 2025-02-19 10:31 a315e0e3

View on Github →

chore: rename ENNReal.to{NN}Real_nat -> ENNReal.to{NN}Real_natCast (#22071) This came up in https://github.com/leanprover-community/mathlib4/pull/22049; zulip discussion.

Estimated changes

Modified Archive/Wiedijk100Theorems/BallotProblem.lean

Modified Mathlib/Analysis/BoxIntegral/UnitPartition.lean

Modified Mathlib/Analysis/Normed/Lp/PiLp.lean

Modified Mathlib/Analysis/Normed/Lp/ProdLp.lean

Modified Mathlib/Data/ENNReal/Basic.lean

deleted theorem ENNReal.toNNReal_nat

added theorem ENNReal.toNNReal_natCast

added theorem ENNReal.toNNReal_ofNat

deleted theorem ENNReal.toReal_nat

added theorem ENNReal.toReal_natCast

Modified Mathlib/MeasureTheory/Constructions/HaarToSphere.lean