no goals
α : Type ?u.27142
β : Type ?u.27145
K : Type u_1
inst✝¹ : DivisionMonoid K
inst✝ : HasDistribNeg K
a✝ b✝ a b : K
⊢ b / -a = b * (1 / -a)
rw [← inv_eq_one_div, division_def]
no goals
α : Type ?u.27142
β : Type ?u.27145
K : Type u_1
inst✝¹ : DivisionMonoid K
inst✝ : HasDistribNeg K
a✝ b✝ a b : K
⊢ b * (1 / -a) = b * -(1 / a)
rw [one_div_neg_eq_neg_one_div]
no goals
α : Type ?u.27142
β : Type ?u.27145
K : Type u_1
inst✝¹ : DivisionMonoid K
inst✝ : HasDistribNeg K
a✝ b✝ a b : K
⊢ b * -(1 / a) = -(b * (1 / a))
rw [neg_mul_eq_mul_neg]
no goals
α : Type ?u.27142
β : Type ?u.27145
K : Type u_1
inst✝¹ : DivisionMonoid K
inst✝ : HasDistribNeg K
a✝ b✝ a b : K
⊢ -(b * (1 / a)) = -(b / a)
rw [mul_one_div]