Documentation

LeanAPAP.Mathlib.Data.Real.ENNReal

source
@[simp]
theorem ENNReal.inv_eq_one {x : ENNReal} :
x⁻¹ = 1 ↔ x = 1