case intro
F : Type ?u.34433
α : Type u_1
β : Type ?u.34439
R : Type ?u.34442
inst✝ : DivisionMonoid α
n : ℤ
a : α
⊢ IsSquare ((a * a) ^ n)
F : Type ?u.34433
α : Type u_1
β : Type ?u.34439
R : Type ?u.34442
inst✝ : DivisionMonoid α
a : α
n : ℤ
⊢ IsSquare a → IsSquare (a ^ n)
rintro ⟨a, rfl⟩
no goals
case intro
F : Type ?u.34433
α : Type u_1
β : Type ?u.34439
R : Type ?u.34442
inst✝ : DivisionMonoid α
n : ℤ
a : α
⊢ IsSquare ((a * a) ^ n)
exact ⟨a ^ n, (Commute.refl _).mul_zpow _⟩