Theorem ENNReal.HolderTriple.inv_eq

Modification history

2025-04-10 06:34
Mathlib/Data/ENNReal/Holder.lean
feat: `p / r` and `q / r` are Hölder conjugate if `p, q, r` is a Hölder triple (#23882) …
Modified ENNReal.HolderTriple.inv_eqView on Github →
2025-02-14 03:53
Mathlib/Data/ENNReal/Holder.lean
feat: Hölder triples / conjugates as a type class (#21854) …
Added ENNReal.HolderTriple.inv_eqView on Github →