Results about powers in fields or division rings. #

THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.

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

@[simp]

theorem zpow_bit1_neg {α : Type u_1} [division_ring α] (a : α) (n : ℤ) :

(-a) ^ bit1 n = -a ^ bit1 n

source

theorem odd.neg_zpow {α : Type u_1} [division_ring α] {n : ℤ} (h : odd n) (a : α) :

(-a) ^ n = -a ^ n

source

theorem odd.neg_one_zpow {α : Type u_1} [division_ring α] {n : ℤ} (h : odd n) :

(-1) ^ n = -1