case intro
α : Type u_1
inst✝ : DivisionRing α
a : α
k : ℤ
h : Odd (bit1 k)
⊢ (-a) ^ bit1 k = -a ^ bit1 k
α : Type u_1
inst✝ : DivisionRing α
n : ℤ
h : Odd n
a : α
⊢ (-a) ^ n = -a ^ n
obtain ⟨k, rfl⟩ := h.exists_bit1
no goals
case intro
α : Type u_1
inst✝ : DivisionRing α
a : α
k : ℤ
h : Odd (bit1 k)
⊢ (-a) ^ bit1 k = -a ^ bit1 k
exact zpow_bit1_neg _ _