Commit 2025-03-12 23:13 241c1c00

View on Github →

chore(Data/(E)(NN)Real): address porting notes (#22883) A lot of these porting notes are just plain TODOs, not regressions compared to Lean 3. There are a few remaining porting notes asking for reimplementation of tactic (positivity, norm_num) extensions.

Estimated changes

Modified Mathlib/Data/ENNReal/Action.lean

Modified Mathlib/Data/ENNReal/Basic.lean

Modified Mathlib/Data/ENNReal/Inv.lean

Modified Mathlib/Data/ENNReal/Order.lean

Modified Mathlib/Data/ENNReal/Real.lean

modified def ENNReal.toNNRealHom

modified def ENNReal.toRealHom

Modified Mathlib/Data/NNReal/Basic.lean

Modified Mathlib/Data/NNReal/Defs.lean

deleted theorem NNReal.toNNReal_coe_nat

added theorem Real.toNNReal_coe_nat

Modified Mathlib/Data/Real/Basic.lean

Modified Mathlib/Data/Real/EReal.lean

Modified Mathlib/Data/Real/GoldenRatio.lean

Modified Mathlib/Data/Real/Hyperreal.lean

Modified Mathlib/Data/Real/Sqrt.lean