F : Type ?u.56333
G : Type ?u.56336
α : Type u_1
M : Type ?u.56342
N : Type ?u.56345
inst✝ : DivisionMonoid α
a b c : α
ha : IsUnit a
hb : IsUnit b
⊢ IsUnit (a * b⁻¹)
F : Type ?u.56333
G : Type ?u.56336
α : Type u_1
M : Type ?u.56342
N : Type ?u.56345
inst✝ : DivisionMonoid α
a b c : α
ha : IsUnit a
hb : IsUnit b
⊢ IsUnit (a / b)
rw [div_eq_mul_inv]
no goals
F : Type ?u.56333
G : Type ?u.56336
α : Type u_1
M : Type ?u.56342
N : Type ?u.56345
inst✝ : DivisionMonoid α
a b c : α
ha : IsUnit a
hb : IsUnit b
⊢ IsUnit (a * b⁻¹)
exact ha.mul hb.inv