Theorem Real.nnabs_ofNat

Modification history

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