p q : ℝ
h : IsConjugateExponent p q
this : 1 / p + 1 / q = 1
⊢ q = p / (p - 1)
p q : ℝ
h : IsConjugateExponent p q
⊢ q = p / (p - 1)
have := h.inv_add_inv_conj
p q : ℝ
h : IsConjugateExponent p q
this : q = (1 - 1 / p)⁻¹
⊢ q = p / (p - 1)
p q : ℝ
h : IsConjugateExponent p q
this : 1 / p + 1 / q = 1
⊢ q = p / (p - 1)
rw [← eq_sub_iff_add_eq', one_div, inv_eq_iff_eq_inv] at this
no goals
p q : ℝ
h : IsConjugateExponent p q
this : q = (1 - 1 / p)⁻¹
⊢ q = p / (p - 1)
field_simp [this, h.ne_zero]