case intro
F : Type ?u.50615
α : Type u_1
β : Type ?u.50621
R : Type ?u.50624
inst✝ : Group α
n : ℤ
a : α
⊢ IsSquare (a ^ (n + n))
F : Type ?u.50615
α : Type u_1
β : Type ?u.50621
R : Type ?u.50624
inst✝ : Group α
n : ℤ
⊢ Even n → ∀ (a : α), IsSquare (a ^ n)
rintro ⟨n, rfl⟩ a
no goals
case intro
F : Type ?u.50615
α : Type u_1
β : Type ?u.50621
R : Type ?u.50624
inst✝ : Group α
n : ℤ
a : α
⊢ IsSquare (a ^ (n + n))
exact ⟨a ^ n, zpow_add _ _ _⟩