F : Type ?u.49647
α : Type u_1
β : Type ?u.49653
R : Type ?u.49656
inst✝ : DivisionCommMonoid α
a b : α
ha : IsSquare a
hb : IsSquare b
⊢ IsSquare (a * b⁻¹)
F : Type ?u.49647
α : Type u_1
β : Type ?u.49653
R : Type ?u.49656
inst✝ : DivisionCommMonoid α
a b : α
ha : IsSquare a
hb : IsSquare b
⊢ IsSquare (a / b)
rw [div_eq_mul_inv]
no goals
F : Type ?u.49647
α : Type u_1
β : Type ?u.49653
R : Type ?u.49656
inst✝ : DivisionCommMonoid α
a b : α
ha : IsSquare a
hb : IsSquare b
⊢ IsSquare (a * b⁻¹)
exact ha.mul hb.inv