# 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.

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