Theorem NNReal.HolderTriple.inv_inv_add_inv

Modification history

2026-10-28 10:44
Mathlib/Basic/Real/ConjExponents.lean
chore: replace `exact_mod_cast` with `exact mod_cast` (#44348) …
Modified NNReal.HolderTriple.inv_inv_add_invView on Github →
2025-03-27 13:33
Mathlib/Data/Real/ConjExponents.lean
refactor: merge API for `ENNReal.HolderConjugate` and `{E}{NN}Real.IsConjExponent` (#22944) …
Added NNReal.HolderTriple.inv_inv_add_invView on Github →