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

source
theorem Ring.inverse_pow {M : Type u_3} [MonoidWithZero M] (r : M) (n : ℕ) :
Ring.inverse r ^ n = Ring.inverse (r ^ n)
source
def powMonoidWithZeroHom {M : Type u_3} [CommMonoidWithZero M] {n : ℕ} (hn : n ≠ 0) :
M →*₀ M

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

Equations
Instances For
    source
    @[simp]
    theorem coe_powMonoidWithZeroHom {M : Type u_3} [CommMonoidWithZero M] {n : ℕ} (hn : n ≠ 0) :
    ⇑(powMonoidWithZeroHom hn) = fun (x : M) => x ^ n
    source
    @[simp]
    theorem powMonoidWithZeroHom_apply {M : Type u_3} [CommMonoidWithZero M] {n : ℕ} (hn : n ≠ 0) (a : M) :
    (powMonoidWithZeroHom hn) a = a ^ n
    source
    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
    source
    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
    source
    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
    source
    theorem add_sq {R : Type u_1} [CommSemiring R] (a : R) (b : R) :
    (a + b) ^ 2 = a ^ 2 + 2 * a * b + b ^ 2
    source
    theorem add_sq' {R : Type u_1} [CommSemiring R] (a : R) (b : R) :
    (a + b) ^ 2 = a ^ 2 + b ^ 2 + 2 * a * b
    source
    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.

    source
    theorem neg_one_pow_eq_or (R : Type u_1) [Monoid R] [HasDistribNeg R] (n : ℕ) :
    (-1) ^ n = 1 ∨ (-1) ^ n = -1
    source
    theorem neg_pow {R : Type u_1} [Monoid R] [HasDistribNeg R] (a : R) (n : ℕ) :
    (-a) ^ n = (-1) ^ n * a ^ n
    source
    theorem neg_pow' {R : Type u_1} [Monoid R] [HasDistribNeg R] (a : R) (n : ℕ) :
    (-a) ^ n = a ^ n * (-1) ^ n
    source
    theorem neg_pow_bit0 {R : Type u_1} [Monoid R] [HasDistribNeg R] (a : R) (n : ℕ) :
    (-a) ^ bit0 n = a ^ bit0 n
    source
    @[simp]
    theorem neg_pow_bit1 {R : Type u_1} [Monoid R] [HasDistribNeg R] (a : R) (n : ℕ) :
    (-a) ^ bit1 n = -a ^ bit1 n
    source
    theorem neg_sq {R : Type u_1} [Monoid R] [HasDistribNeg R] (a : R) :
    (-a) ^ 2 = a ^ 2
    source
    theorem neg_one_sq {R : Type u_1} [Monoid R] [HasDistribNeg R] :
    (-1) ^ 2 = 1
    source
    theorem neg_pow_two {R : Type u_1} [Monoid R] [HasDistribNeg R] (a : R) :
    (-a) ^ 2 = a ^ 2

    Alias of neg_sq.

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

    Alias of neg_one_sq.

    source
    @[simp]
    theorem zpow_bit0_neg {R : Type u_1} [DivisionMonoid R] [HasDistribNeg R] (a : R) (n : ℤ) :
    (-a) ^ bit0 n = a ^ bit0 n
    source
    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)
    source
    @[simp]
    theorem neg_one_pow_mul_eq_zero_iff {R : Type u_1} [Ring R] {n : ℕ} {r : R} :
    (-1) ^ n * r = 0 ↔ r = 0
    source
    @[simp]
    theorem mul_neg_one_pow_eq_zero_iff {R : Type u_1} [Ring R] {n : ℕ} {r : R} :
    r * (-1) ^ n = 0 ↔ r = 0
    source
    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
    source
    @[simp]
    theorem sq_eq_one_iff {R : Type u_1} [Ring R] {a : R} [NoZeroDivisors R] :
    a ^ 2 = 1 ↔ a = 1 ∨ a = -1
    source
    theorem sq_ne_one_iff {R : Type u_1} [Ring R] {a : R} [NoZeroDivisors R] :
    a ^ 2 ≠ 1 ↔ a ≠ 1 ∧ a ≠ -1
    source
    theorem neg_one_pow_eq_pow_mod_two {R : Type u_1} [Ring R] (n : ℕ) :
    (-1) ^ n = (-1) ^ (n % 2)
    source
    theorem sq_sub_sq {R : Type u_1} [CommRing R] (a : R) (b : R) :
    a ^ 2 - b ^ 2 = (a + b) * (a - b)
    source
    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.

    source
    theorem sub_sq {R : Type u_1} [CommRing R] (a : R) (b : R) :
    (a - b) ^ 2 = a ^ 2 - 2 * a * b + b ^ 2
    source
    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.

    source
    theorem sub_sq' {R : Type u_1} [CommRing R] (a : R) (b : R) :
    (a - b) ^ 2 = a ^ 2 + b ^ 2 - 2 * a * b
    source
    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
    source
    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
    source
    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
    source
    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