case intro
F : Type ?u.20712
α : Type u_1
β : Type ?u.20718
R : Type ?u.20721
inst✝¹ : Monoid α
a✝ : α
inst✝ : HasDistribNeg α
c : ℕ
a : α
⊢ (-a) ^ (c + c) = a ^ (c + c)
F : Type ?u.20712
α : Type u_1
β : Type ?u.20718
R : Type ?u.20721
inst✝¹ : Monoid α
n : ℕ
a : α
inst✝ : HasDistribNeg α
⊢ Even n → ∀ (a : α), (-a) ^ n = a ^ n
rintro ⟨c, rfl⟩ a
no goals
case intro
F : Type ?u.20712
α : Type u_1
β : Type ?u.20718
R : Type ?u.20721
inst✝¹ : Monoid α
a✝ : α
inst✝ : HasDistribNeg α
c : ℕ
a : α
⊢ (-a) ^ (c + c) = a ^ (c + c)
simp_rw [← two_mul, pow_mul, neg_sq]