Mathlib Changelog
v4
Changelog
About
Github
Theorem
ENNReal.HolderConjugate.inv_add_inv_eq_one
Modification history
2025-02-14 03:53
Mathlib/Data/ENNReal/Holder.lean
feat: Hölder triples / conjugates as a type class (#21854) …
Added
ENNReal.HolderConjugate.inv_add_inv_eq_one
View on Github →