Commit 2026-05-20 15:22 5feb5abb

View on Github →

feat(Data/NNReal): nnabs n = n for n : ℕ (#39577) From MeanFourier

Estimated changes

added theorem Real.nnabs_natCast
added theorem Real.nnabs_ofNat
deleted theorem Real.toNNReal_coe_nat
added theorem Real.toNNReal_natCast