ι : Type ?u.9146
α : Type u_1
β : Type ?u.9152
inst✝ : LinearOrderedSemifield α
a b c d e : α
m n : ℤ
ha : 0 < a
hb : 0 < b
⊢ 0 < a * b⁻¹
ι : Type ?u.9146
α : Type u_1
β : Type ?u.9152
inst✝ : LinearOrderedSemifield α
a b c d e : α
m n : ℤ
ha : 0 < a
hb : 0 < b
⊢ 0 < a / b
rw [div_eq_mul_inv]
no goals
ι : Type ?u.9146
α : Type u_1
β : Type ?u.9152
inst✝ : LinearOrderedSemifield α
a b c d e : α
m n : ℤ
ha : 0 < a
hb : 0 < b
⊢ 0 < a * b⁻¹
exact mul_pos ha (inv_pos.2 hb)