Semirings and rings

This file gives lemmas about semirings, rings and domains. This is analogous to Mathlib/Algebra/Group/Basic.lean, the difference being that the former is about + and * separately, while the present file is about their interaction.

For the definitions of semirings and rings see Mathlib/Algebra/Ring/Defs.lean.

@[simp]

theorem Commute.add_right {R : Type u} [Distrib R] {a b c : R} : Commute a b → Commute a c → Commute a (b + c)

@[simp]

theorem Commute.add_left {R : Type u} [Distrib R] {a b c : R} : Commute a c → Commute b c → Commute (a + b) c

theorem Commute.mul_self_sub_mul_self_eq {R : Type u} [NonUnitalNonAssocRing R] {a b : R} (h : Commute a b) : a * a - b * b = (a + b) * (a - b)

Representation of a difference of two squares of commuting elements as a product.

theorem Commute.mul_self_sub_mul_self_eq' {R : Type u} [NonUnitalNonAssocRing R] {a b : R} (h : Commute a b) : a * a - b * b = (a - b) * (a + b)

theorem Commute.mul_self_eq_mul_self_iff {R : Type u} [NonUnitalNonAssocRing R] [NoZeroDivisors R] {a b : R} (h : Commute a b) : a * a = b * b ↔ a = b ∨ a = -b

theorem Commute.neg_right {R : Type u} [Mul R] [HasDistribNeg R] {a b : R} : Commute a b → Commute a (-b)

@[simp]

theorem Commute.neg_right_iff {R : Type u} [Mul R] [HasDistribNeg R] {a b : R} : Commute a (-b) ↔ Commute a b

theorem Commute.neg_left {R : Type u} [Mul R] [HasDistribNeg R] {a b : R} : Commute a b → Commute (-a) b

@[simp]

theorem Commute.neg_left_iff {R : Type u} [Mul R] [HasDistribNeg R] {a b : R} : Commute (-a) b ↔ Commute a b

theorem Commute.neg_one_right {R : Type u} [MulOneClass R] [HasDistribNeg R] (a : R) : Commute a (-1)

theorem Commute.neg_one_left {R : Type u} [MulOneClass R] [HasDistribNeg R] (a : R) : Commute (-1) a

@[simp]

theorem Commute.sub_right {R : Type u} [NonUnitalNonAssocRing R] {a b c : R} : Commute a b → Commute a c → Commute a (b - c)

@[simp]

theorem Commute.sub_left {R : Type u} [NonUnitalNonAssocRing R] {a b c : R} : Commute a c → Commute b c → Commute (a - b) c

theorem Commute.add_sq {R : Type u} [Semiring R] {a b : R} (h : Commute a b) : (a + b) ^ 2 = a ^ 2 + 2 * a * b + b ^ 2

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

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

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

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

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

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

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

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

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

Alias of neg_sq.

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

Alias of neg_one_sq.

@[simp]

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

@[simp]

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

theorem neg_one_pow_eq_pow_mod_two {R : Type u} [Ring R] (n : ℕ) : (-1) ^ n = (-1) ^ (n % 2)

@[simp]

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

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

theorem mul_self_sub_mul_self {R : Type u} [NonUnitalNonAssocCommRing R] (a b : R) : a * a - b * b = (a + b) * (a - b)

Representation of a difference of two squares in a commutative ring as a product.

theorem mul_self_sub_one {R : Type u} [NonAssocRing R] (a : R) : a * a - 1 = (a + 1) * (a - 1)

theorem mul_self_eq_mul_self_iff {R : Type u} [NonUnitalNonAssocCommRing R] [NoZeroDivisors R] {a b : R} : a * a = b * b ↔ a = b ∨ a = -b

theorem mul_self_eq_one_iff {R : Type u} [NonAssocRing R] [NoZeroDivisors R] {a : R} : a * a = 1 ↔ a = 1 ∨ a = -1

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

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

Alias of sq_sub_sq.

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

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

Alias of sub_sq.

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

theorem sub_sq_comm {R : Type u} [CommRing R] (a b : R) : (a - b) ^ 2 = (b - a) ^ 2

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

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

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

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

theorem Units.inv_eq_self_iff {R : Type u} [Ring R] [NoZeroDivisors R] (u : Rˣ) : u⁻¹ = u ↔ u = 1 ∨ u = -1

In the unit group of an integral domain, a unit is its own inverse iff the unit is one or one's additive inverse.

@[implicit_reducible, instance 100]

instance Ring.instBracket {R : Type u} [NonUnitalNonAssocRing R] : Bracket R R

theorem Ring.lie_def {R : Type u} [NonUnitalNonAssocRing R] (x y : R) : ⁅x, y⁆ = x * y - y * x

theorem commute_iff_lie_eq {R : Type u} [NonUnitalNonAssocRing R] {x y : R} : Commute x y ↔ ⁅x, y⁆ = 0

theorem Commute.lie_eq {R : Type u} [NonUnitalNonAssocRing R] {x y : R} (h : Commute x y) : ⁅x, y⁆ = 0