Theorem Real.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 Real.HolderTriple.holderConjugate_div_divView on Github →