case intro
F : Type ?u.40950
α : Type u_1
β : Type ?u.40956
R : Type ?u.40959
inst✝¹ : DivisionMonoid α
a✝ : α
inst✝ : HasDistribNeg α
c : ℤ
a : α
⊢ (-a) ^ (c + c) = a ^ (c + c)
F : Type ?u.40950
α : Type u_1
β : Type ?u.40956
R : Type ?u.40959
inst✝¹ : DivisionMonoid α
a : α
inst✝ : HasDistribNeg α
n : ℤ
⊢ Even n → ∀ (a : α), (-a) ^ n = a ^ n
rintro ⟨c, rfl⟩ a
no goals
case intro
F : Type ?u.40950
α : Type u_1
β : Type ?u.40956
R : Type ?u.40959
inst✝¹ : DivisionMonoid α
a✝ : α
inst✝ : HasDistribNeg α
c : ℤ
a : α
⊢ (-a) ^ (c + c) = a ^ (c + c)
exact zpow_bit0_neg _ _