Results about powers in fields or division rings.

This file exists to ensure we can define Field with minimal imports, so contains some lemmas about powers of elements which need imports beyond those needed for the basic definition.

@[simp]

theorem zpow_bit1_neg {α : Type u_1} [DivisionRing α] (a : α) (n : ℤ) : (-a) ^ bit1 n = -a ^ bit1 n

theorem Odd.neg_zpow {α : Type u_1} [DivisionRing α] {n : ℤ} (h : Odd n) (a : α) : (-a) ^ n = -a ^ n

theorem Odd.neg_one_zpow {α : Type u_1} [DivisionRing α] {n : ℤ} (h : Odd n) : (-1) ^ n = -1