case intro
F : Type ?u.8146
α : Type u_1
β : Type ?u.8152
R : Type ?u.8155
inst✝ : Monoid α
n✝ n : ℕ
a : α
⊢ IsSquare ((a * a) ^ n)
F : Type ?u.8146
α : Type u_1
β : Type ?u.8152
R : Type ?u.8155
inst✝ : Monoid α
n✝ : ℕ
a : α
n : ℕ
⊢ IsSquare a → IsSquare (a ^ n)
rintro ⟨a, rfl⟩
no goals
case intro
F : Type ?u.8146
α : Type u_1
β : Type ?u.8152
R : Type ?u.8155
inst✝ : Monoid α
n✝ n : ℕ
a : α
⊢ IsSquare ((a * a) ^ n)
exact ⟨a ^ n, (Commute.refl _).mul_pow _⟩