Theorem: ENNReal.conjExponent_eq_one (ForML/LpHoelder.lean)

State before:
p q : ℝ≥0∞
⊢ conjExponent p = 1 ↔ p = ⊤
Tactic:
simp [conjExponent, inv_eq_iff_eq_inv]
State after:
no goals