Theorem NNReal.toReal_ne

Modification history

2026-02-22 22:01
Mathlib/Data/NNReal/Basic.lean
feat(Tactic): `linarith` and `rify` for NNReal (#35155)
Added NNReal.toReal_neView on Github →