Mathlib Changelog
v4
Changelog
About
Github
Theorem
NNReal.HolderTriple.holderConjugate_div_div
Modification history
2025-04-10 06:34
Mathlib/Data/Real/ConjExponents.lean
feat: `p / r` and `q / r` are Hölder conjugate if `p, q, r` is a Hölder triple (#23882) …
Added
NNReal.HolderTriple.holderConjugate_div_div
View on Github →