Theorem Real.toNNReal_natCast

Modification history

2026-05-20 15:22
Mathlib/Data/NNReal/Defs.lean
feat(Data/NNReal): `nnabs n = n` for `n : ℕ` (#39577) …
Added Real.toNNReal_natCastView on Github →