Theorem ENNReal.inv_mul_ne_top

Modification history

2025-05-27 14:09
Mathlib/Data/ENNReal/Inv.lean
feat(Tactic/Finiteness): tag more lemmas (#25086) …
Modified ENNReal.inv_mul_ne_topView on Github →
2024-07-05 08:06
Mathlib/Data/ENNReal/Inv.lean
feat(ENNReal/Inv): add lemmas about `a * a⁻¹` (#14423) …
Added ENNReal.inv_mul_ne_topView on Github →