Theorem Real.toNNReal_coe_nat

Modification history

2026-05-20 15:22
Mathlib/Data/NNReal/Defs.lean
feat(Data/NNReal): `nnabs n = n` for `n : ℕ` (#39577) …
Deleted Real.toNNReal_coe_natView on Github →
2025-03-12 23:13
Mathlib/Data/NNReal/Defs.lean
chore(Data/(E)(NN)Real): address porting notes (#22883) …
Added Real.toNNReal_coe_natView on Github →