no goals
α : Type ?u.23152
β : Type ?u.23155
K : Type u_1
inst✝¹ : DivisionMonoid K
inst✝ : HasDistribNeg K
a✝ b a : K
⊢ 1 / -a = 1 / (-1 * a)
rw [neg_eq_neg_one_mul]
no goals
α : Type ?u.23152
β : Type ?u.23155
K : Type u_1
inst✝¹ : DivisionMonoid K
inst✝ : HasDistribNeg K
a✝ b a : K
⊢ 1 / (-1 * a) = 1 / a * (1 / -1)
rw [one_div_mul_one_div_rev]
no goals
α : Type ?u.23152
β : Type ?u.23155
K : Type u_1
inst✝¹ : DivisionMonoid K
inst✝ : HasDistribNeg K
a✝ b a : K
⊢ 1 / a * (1 / -1) = 1 / a * -1
rw [one_div_neg_one_eq_neg_one]
no goals
α : Type ?u.23152
β : Type ?u.23155
K : Type u_1
inst✝¹ : DivisionMonoid K
inst✝ : HasDistribNeg K
a✝ b a : K
⊢ 1 / a * -1 = -(1 / a)
rw [mul_neg, mul_one]