p q : ℝ
h : IsConjugateExponent p q
⊢ 1 < p / (p - 1)
p q : ℝ
h : IsConjugateExponent p q
⊢ 1 < q
rw [h.conj_eq]
no goals
p q : ℝ
h : IsConjugateExponent p q
⊢ 1 < p / (p - 1)
exact (one_lt_div h.sub_one_pos).mpr (sub_one_lt p)
no goals
p q : ℝ
h : IsConjugateExponent p q
⊢ 1 / q + 1 / p = 1
simpa [add_comm] using h.inv_add_inv_conj