Power operations on monoids with zero, semirings, and rings

This file provides additional lemmas about the natural power operator on rings and semirings. Further lemmas about ordered semirings and rings can be found in Algebra.GroupPower.Lemmas.

theorem zero_pow {M : Type u_3} [MonoidWithZero M] {n : ℕ} : 0 < n → 0 ^ n = 0

@[simp]

theorem zero_pow' {M : Type u_3} [MonoidWithZero M] (n : ℕ) : n ≠ 0 → 0 ^ n = 0

theorem zero_pow_eq {M : Type u_3} [MonoidWithZero M] (n : ℕ) : 0 ^ n = if n = 0 then 1 else 0

theorem pow_eq_zero_of_le {M : Type u_3} [MonoidWithZero M] {x : M} {n : ℕ} {m : ℕ} (hn : n ≤ m) (hx : x ^ n = 0) : x ^ m = 0

theorem pow_eq_zero {M : Type u_3} [MonoidWithZero M] [NoZeroDivisors M] {x : M} {n : ℕ} (H : x ^ n = 0) : x = 0

@[simp]

theorem pow_eq_zero_iff {M : Type u_3} [MonoidWithZero M] [NoZeroDivisors M] {a : M} {n : ℕ} (hn : 0 < n) : a ^ n = 0 ↔ a = 0

theorem pow_eq_zero_iff' {M : Type u_3} [MonoidWithZero M] [NoZeroDivisors M] [Nontrivial M] {a : M} {n : ℕ} : a ^ n = 0 ↔ a = 0 ∧ n ≠ 0

theorem pow_ne_zero_iff {M : Type u_3} [MonoidWithZero M] [NoZeroDivisors M] {a : M} {n : ℕ} (hn : 0 < n) : a ^ n ≠ 0 ↔ a ≠ 0

theorem ne_zero_pow {M : Type u_3} [MonoidWithZero M] {a : M} {n : ℕ} (hn : n ≠ 0) : a ^ n ≠ 0 → a ≠ 0

theorem pow_ne_zero {M : Type u_3} [MonoidWithZero M] [NoZeroDivisors M] {a : M} (n : ℕ) (h : a ≠ 0) : a ^ n ≠ 0

instance NeZero.pow {M : Type u_3} [MonoidWithZero M] [NoZeroDivisors M] {x : M} [NeZero x] {n : ℕ} : NeZero (x ^ n)

Equations

• @NeZero.pow = @NeZero.pow.proof_1

theorem sq_eq_zero_iff {M : Type u_3} [MonoidWithZero M] [NoZeroDivisors M] {a : M} : a ^ 2 = 0 ↔ a = 0

@[simp]

theorem zero_pow_eq_zero {M : Type u_3} [MonoidWithZero M] [Nontrivial M] {n : ℕ} : 0 ^ n = 0 ↔ 0 < n

theorem Ring.inverse_pow {M : Type u_3} [MonoidWithZero M] (r : M) (n : ℕ) : Ring.inverse r ^ n = Ring.inverse (r ^ n)

def powMonoidWithZeroHom {M : Type u_3} [CommMonoidWithZero M] {n : ℕ} (hn : 0 < n) : M →*₀ M

We define x ↦ x^n (for positive n : ℕ) as a MonoidWithZeroHom

Equations

• One or more equations did not get rendered due to their size.

@[simp]

theorem coe_powMonoidWithZeroHom {M : Type u_3} [CommMonoidWithZero M] {n : ℕ} (hn : 0 < n) : ↑(powMonoidWithZeroHom hn) = fun x => x ^ n

@[simp]

theorem powMonoidWithZeroHom_apply {M : Type u_3} [CommMonoidWithZero M] {n : ℕ} (hn : 0 < n) (a : M) : ↑(powMonoidWithZeroHom hn) a = a ^ n

theorem pow_dvd_pow_iff {R : Type u_1} [CancelCommMonoidWithZero R] {x : R} {n : ℕ} {m : ℕ} (h0 : x ≠ 0) (h1 : ¬IsUnit x) : x ^ n ∣ x ^ m ↔ n ≤ m

theorem RingHom.map_pow {R : Type u_1} {S : Type u_2} [Semiring R] [Semiring S] (f : R →+* S) (a : R) (n : ℕ) : ↑f (a ^ n) = ↑f a ^ n

theorem min_pow_dvd_add {R : Type u_1} [Semiring R] {n : ℕ} {m : ℕ} {a : R} {b : R} {c : R} (ha : c ^ n ∣ a) (hb : c ^ m ∣ b) : c ^ min n m ∣ a + b

theorem add_sq {R : Type u_1} [CommSemiring R] (a : R) (b : R) : (a + b) ^ 2 = a ^ 2 + 2 * a * b + b ^ 2

theorem add_sq' {R : Type u_1} [CommSemiring R] (a : R) (b : R) : (a + b) ^ 2 = a ^ 2 + b ^ 2 + 2 * a * b

theorem add_pow_two {R : Type u_1} [CommSemiring R] (a : R) (b : R) : (a + b) ^ 2 = a ^ 2 + 2 * a * b + b ^ 2

Alias of add_sq.

theorem neg_one_pow_eq_or (R : Type u_1) [Monoid R] [HasDistribNeg R] (n : ℕ) : (-1) ^ n = 1 ∨ (-1) ^ n = -1

theorem neg_pow {R : Type u_1} [Monoid R] [HasDistribNeg R] (a : R) (n : ℕ) : (-a) ^ n = (-1) ^ n * a ^ n

theorem neg_pow' {R : Type u_1} [Monoid R] [HasDistribNeg R] (a : R) (n : ℕ) : (-a) ^ n = a ^ n * (-1) ^ n

theorem neg_pow_bit0 {R : Type u_1} [Monoid R] [HasDistribNeg R] (a : R) (n : ℕ) : (-a) ^ bit0 n = a ^ bit0 n

@[simp]

theorem neg_pow_bit1 {R : Type u_1} [Monoid R] [HasDistribNeg R] (a : R) (n : ℕ) : (-a) ^ bit1 n = -a ^ bit1 n

theorem neg_sq {R : Type u_1} [Monoid R] [HasDistribNeg R] (a : R) : (-a) ^ 2 = a ^ 2

theorem neg_one_sq {R : Type u_1} [Monoid R] [HasDistribNeg R] : (-1) ^ 2 = 1

theorem neg_pow_two {R : Type u_1} [Monoid R] [HasDistribNeg R] (a : R) : (-a) ^ 2 = a ^ 2

Alias of neg_sq.

theorem neg_one_pow_two {R : Type u_1} [Monoid R] [HasDistribNeg R] : (-1) ^ 2 = 1

Alias of neg_one_sq.

theorem Commute.sq_sub_sq {R : Type u_1} [Ring R] {a : R} {b : R} (h : Commute a b) : a ^ 2 - b ^ 2 = (a + b) * (a - b)

@[simp]

theorem neg_one_pow_mul_eq_zero_iff {R : Type u_1} [Ring R] {n : ℕ} {r : R} : (-1) ^ n * r = 0 ↔ r = 0

@[simp]

theorem mul_neg_one_pow_eq_zero_iff {R : Type u_1} [Ring R] {n : ℕ} {r : R} : r * (-1) ^ n = 0 ↔ r = 0

theorem Commute.sq_eq_sq_iff_eq_or_eq_neg {R : Type u_1} [Ring R] {a : R} {b : R} [NoZeroDivisors R] (h : Commute a b) : a ^ 2 = b ^ 2 ↔ a = b ∨ a = -b

@[simp]

theorem sq_eq_one_iff {R : Type u_1} [Ring R] {a : R} [NoZeroDivisors R] : a ^ 2 = 1 ↔ a = 1 ∨ a = -1

theorem sq_ne_one_iff {R : Type u_1} [Ring R] {a : R} [NoZeroDivisors R] : a ^ 2 ≠ 1 ↔ a ≠ 1 ∧ a ≠ -1

theorem sq_sub_sq {R : Type u_1} [CommRing R] (a : R) (b : R) : a ^ 2 - b ^ 2 = (a + b) * (a - b)

theorem pow_two_sub_pow_two {R : Type u_1} [CommRing R] (a : R) (b : R) : a ^ 2 - b ^ 2 = (a + b) * (a - b)

Alias of sq_sub_sq.

theorem sub_sq {R : Type u_1} [CommRing R] (a : R) (b : R) : (a - b) ^ 2 = a ^ 2 - 2 * a * b + b ^ 2

theorem sub_pow_two {R : Type u_1} [CommRing R] (a : R) (b : R) : (a - b) ^ 2 = a ^ 2 - 2 * a * b + b ^ 2

Alias of sub_sq.

theorem sub_sq' {R : Type u_1} [CommRing R] (a : R) (b : R) : (a - b) ^ 2 = a ^ 2 + b ^ 2 - 2 * a * b

theorem sq_eq_sq_iff_eq_or_eq_neg {R : Type u_1} [CommRing R] [NoZeroDivisors R] {a : R} {b : R} : a ^ 2 = b ^ 2 ↔ a = b ∨ a = -b

theorem eq_or_eq_neg_of_sq_eq_sq {R : Type u_1} [CommRing R] [NoZeroDivisors R] (a : R) (b : R) : a ^ 2 = b ^ 2 → a = b ∨ a = -b

theorem Units.sq_eq_sq_iff_eq_or_eq_neg {R : Type u_1} [CommRing R] [NoZeroDivisors R] {a : Rˣ} {b : Rˣ} : a ^ 2 = b ^ 2 ↔ a = b ∨ a = -b

theorem Units.eq_or_eq_neg_of_sq_eq_sq {R : Type u_1} [CommRing R] [NoZeroDivisors R] (a : Rˣ) (b : Rˣ) (h : a ^ 2 = b ^ 2) : a = b ∨ a = -b