Documentation

Mathlib.Algebra.GroupPower.Ring

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_1} [inst : MonoidWithZero M] {n : } :
0 < n0 ^ n = 0
@[simp]
theorem zero_pow' {M : Type u_1} [inst : MonoidWithZero M] (n : ) :
n 00 ^ n = 0
theorem zero_pow_eq {M : Type u_1} [inst : MonoidWithZero M] (n : ) :
0 ^ n = if n = 0 then 1 else 0
theorem pow_eq_zero_of_le {M : Type u_1} [inst : MonoidWithZero M] {x : M} {n : } {m : } (hn : n m) (hx : x ^ n = 0) :
x ^ m = 0
theorem pow_eq_zero {M : Type u_1} [inst : MonoidWithZero M] [inst : NoZeroDivisors M] {x : M} {n : } (H : x ^ n = 0) :
x = 0
@[simp]
theorem pow_eq_zero_iff {M : Type u_1} [inst : MonoidWithZero M] [inst : NoZeroDivisors M] {a : M} {n : } (hn : 0 < n) :
a ^ n = 0 a = 0
theorem pow_eq_zero_iff' {M : Type u_1} [inst : MonoidWithZero M] [inst : NoZeroDivisors M] [inst : Nontrivial M] {a : M} {n : } :
a ^ n = 0 a = 0 n 0
theorem pow_ne_zero_iff {M : Type u_1} [inst : MonoidWithZero M] [inst : NoZeroDivisors M] {a : M} {n : } (hn : 0 < n) :
a ^ n 0 a 0
theorem ne_zero_pow {M : Type u_1} [inst : MonoidWithZero M] {a : M} {n : } (hn : n 0) :
a ^ n 0a 0
theorem pow_ne_zero {M : Type u_1} [inst : MonoidWithZero M] [inst : NoZeroDivisors M] {a : M} (n : ) (h : a 0) :
a ^ n 0
instance NeZero.pow {M : Type u_1} [inst : MonoidWithZero M] [inst : NoZeroDivisors M] {x : M} [inst : NeZero x] {n : } :
NeZero (x ^ n)
Equations
theorem sq_eq_zero_iff {M : Type u_1} [inst : MonoidWithZero M] [inst : NoZeroDivisors M] {a : M} :
a ^ 2 = 0 a = 0
@[simp]
theorem zero_pow_eq_zero {M : Type u_1} [inst : MonoidWithZero M] [inst : Nontrivial M] {n : } :
0 ^ n = 0 0 < n
theorem Ring.inverse_pow {M : Type u_1} [inst : MonoidWithZero M] (r : M) (n : ) :
def powMonoidWithZeroHom {M : Type u_1} [inst : CommMonoidWithZero M] {n : } (hn : 0 < n) :

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_1} [inst : CommMonoidWithZero M] {n : } (hn : 0 < n) :
↑(powMonoidWithZeroHom hn) = fun x => x ^ n
@[simp]
theorem powMonoidWithZeroHom_apply {M : Type u_1} [inst : CommMonoidWithZero M] {n : } (hn : 0 < n) (a : M) :
↑(powMonoidWithZeroHom hn) a = a ^ n
theorem pow_dvd_pow_iff {R : Type u_1} [inst : 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} [inst : Semiring R] [inst : Semiring S] (f : R →+* S) (a : R) (n : ) :
f (a ^ n) = f a ^ n
theorem min_pow_dvd_add {R : Type u_1} [inst : 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} [inst : CommSemiring R] (a : R) (b : R) :
(a + b) ^ 2 = a ^ 2 + 2 * a * b + b ^ 2
theorem add_sq' {R : Type u_1} [inst : CommSemiring R] (a : R) (b : R) :
(a + b) ^ 2 = a ^ 2 + b ^ 2 + 2 * a * b
theorem add_pow_two {R : Type u_1} [inst : 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) [inst : Monoid R] [inst : HasDistribNeg R] (n : ) :
(-1) ^ n = 1 (-1) ^ n = -1
theorem neg_pow {R : Type u_1} [inst : Monoid R] [inst : HasDistribNeg R] (a : R) (n : ) :
(-a) ^ n = (-1) ^ n * a ^ n
@[simp]
theorem neg_pow_bit0 {R : Type u_1} [inst : Monoid R] [inst : HasDistribNeg R] (a : R) (n : ) :
(-a) ^ bit0 n = a ^ bit0 n
@[simp]
theorem neg_pow_bit1 {R : Type u_1} [inst : Monoid R] [inst : HasDistribNeg R] (a : R) (n : ) :
(-a) ^ bit1 n = -a ^ bit1 n
@[simp]
theorem neg_sq {R : Type u_1} [inst : Monoid R] [inst : HasDistribNeg R] (a : R) :
(-a) ^ 2 = a ^ 2
theorem neg_one_sq {R : Type u_1} [inst : Monoid R] [inst : HasDistribNeg R] :
(-1) ^ 2 = 1
theorem neg_pow_two {R : Type u_1} [inst : Monoid R] [inst : HasDistribNeg R] (a : R) :
(-a) ^ 2 = a ^ 2

Alias of neg_sq.

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

Alias of neg_one_sq.

theorem Commute.sq_sub_sq {R : Type u_1} [inst : 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} [inst : Ring R] {n : } {r : R} :
(-1) ^ n * r = 0 r = 0
@[simp]
theorem mul_neg_one_pow_eq_zero_iff {R : Type u_1} [inst : 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} [inst : Ring R] {a : R} {b : R} [inst : NoZeroDivisors R] (h : Commute a b) :
a ^ 2 = b ^ 2 a = b a = -b
@[simp]
theorem sq_eq_one_iff {R : Type u_1} [inst : Ring R] {a : R} [inst : NoZeroDivisors R] :
a ^ 2 = 1 a = 1 a = -1
theorem sq_ne_one_iff {R : Type u_1} [inst : Ring R] {a : R} [inst : NoZeroDivisors R] :
a ^ 2 1 a 1 a -1
theorem sq_sub_sq {R : Type u_1} [inst : CommRing R] (a : R) (b : R) :
a ^ 2 - b ^ 2 = (a + b) * (a - b)
theorem pow_two_sub_pow_two {R : Type u_1} [inst : 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} [inst : CommRing R] (a : R) (b : R) :
(a - b) ^ 2 = a ^ 2 - 2 * a * b + b ^ 2
theorem sub_pow_two {R : Type u_1} [inst : 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} [inst : 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} [inst : CommRing R] [inst : 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} [inst : CommRing R] [inst : NoZeroDivisors R] (a : R) (b : R) :
a ^ 2 = b ^ 2a = b a = -b
theorem Units.sq_eq_sq_iff_eq_or_eq_neg {R : Type u_1} [inst : CommRing R] [inst : 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} [inst : CommRing R] [inst : NoZeroDivisors R] (a : Rˣ) (b : Rˣ) (h : a ^ 2 = b ^ 2) :
a = b a = -b