Theorem NNReal.coe_ne_zero

Modification history

2024-02-12 08:25

Mathlib/Data/Real/NNReal.lean

feat: Complete `NNReal` coercion lemmas (#10214) …

Modified NNReal.coe_ne_zero View on Github →

2023-02-20 08:04

Mathlib/Data/Real/NNReal.lean

feat: port Data.Real.NNReal (#2234)

Added NNReal.coe_ne_zero View on Github →