Theorem NNReal.natCast_iSup

Modification history

2026-01-30 10:38
Mathlib/Data/NNReal/Basic.lean
feat(NNReal): supremum commutes with Nat.cast (#34467) …
Added NNReal.natCast_iSupView on Github →