Commit 2024-03-23 15:40 a0e02a93

View on Github →

feat: Real.toNNReal_abs (#11606) Partially forward-port https://github.com/leanprover-community/mathlib/pull/16976 Also fix an unused argument that somehow made it to master, likely from #10661.

Estimated changes

Modified Mathlib/Analysis/Distribution/SchwartzSpace.lean

Modified Mathlib/Data/Real/NNReal.lean

added theorem Real.toNNReal_abs