Commit 2024-07-05 08:06 d66f005e
View on Github →feat(ENNReal/Inv): add lemmas about a * a⁻¹ (#14423)
Cherry-picked from #11143
and moved to reuse ENNReal.div_self_le_one.
feat(ENNReal/Inv): add lemmas about a * a⁻¹ (#14423)
Cherry-picked from #11143
and moved to reuse ENNReal.div_self_le_one.