case intro
F : Type ?u.92455
α : Type u_1
β : Type ?u.92461
R : Type ?u.92464
inst✝¹ : Monoid α
inst✝ : HasDistribNeg α
a✝ : α
c : ℕ
a : α
⊢ (-a) ^ (2 * c + 1) = -a ^ (2 * c + 1)
F : Type ?u.92455
α : Type u_1
β : Type ?u.92461
R : Type ?u.92464
inst✝¹ : Monoid α
inst✝ : HasDistribNeg α
a : α
n : ℕ
⊢ Odd n → ∀ (a : α), (-a) ^ n = -a ^ n
rintro ⟨c, rfl⟩ a
no goals
case intro
F : Type ?u.92455
α : Type u_1
β : Type ?u.92461
R : Type ?u.92464
inst✝¹ : Monoid α
inst✝ : HasDistribNeg α
a✝ : α
c : ℕ
a : α
⊢ (-a) ^ (2 * c + 1) = -a ^ (2 * c + 1)
simp_rw [pow_add, pow_mul, neg_sq, pow_one, mul_neg]