Semirings and rings #

This file gives lemmas about semirings, rings and domains. This is analogous to Mathlib.Algebra.Group.Basic, 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.

source

@[simp]

theorem Commute.add_right {R : Type x} [Distrib R] {a : R} {b : R} {c : R} :

Commute a b → Commute a c → Commute a (b + c)

source

@[simp]

theorem Commute.add_left {R : Type x} [Distrib R] {a : R} {b : R} {c : R} :

Commute a c → Commute b c → Commute (a + b) c

source

@[deprecated]

theorem Commute.bit0_right {R : Type x} [Distrib R] {x : R} {y : R} (h : Commute x y) :

Commute x (bit0 y)

source

@[deprecated]

theorem Commute.bit0_left {R : Type x} [Distrib R] {x : R} {y : R} (h : Commute x y) :

Commute (bit0 x) y

source

@[deprecated]

theorem Commute.bit1_right {R : Type x} [NonAssocSemiring R] {x : R} {y : R} (h : Commute x y) :

Commute x (bit1 y)

source

@[deprecated]

theorem Commute.bit1_left {R : Type x} [NonAssocSemiring R] {x : R} {y : R} (h : Commute x y) :

Commute (bit1 x) y

source

theorem Commute.mul_self_sub_mul_self_eq {R : Type x} [NonUnitalNonAssocRing R] {a : R} {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.

source

theorem Commute.mul_self_sub_mul_self_eq' {R : Type x} [NonUnitalNonAssocRing R] {a : R} {b : R} (h : Commute a b) :

a * a - b * b = (a - b) * (a + b)

source

theorem Commute.mul_self_eq_mul_self_iff {R : Type x} [NonUnitalNonAssocRing R] [NoZeroDivisors R] {a : R} {b : R} (h : Commute a b) :

a * a = b * b ↔ a = b ∨ a = -b

source

theorem Commute.neg_right {R : Type x} [Mul R] [HasDistribNeg R] {a : R} {b : R} :

Commute a b → Commute a (-b)

source

@[simp]

theorem Commute.neg_right_iff {R : Type x} [Mul R] [HasDistribNeg R] {a : R} {b : R} :

Commute a (-b) ↔ Commute a b

source

theorem Commute.neg_left {R : Type x} [Mul R] [HasDistribNeg R] {a : R} {b : R} :

Commute a b → Commute (-a) b

source

@[simp]

theorem Commute.neg_left_iff {R : Type x} [Mul R] [HasDistribNeg R] {a : R} {b : R} :

Commute (-a) b ↔ Commute a b

source

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

Commute a (-1)

source

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

Commute (-1) a

source

@[simp]

theorem Commute.sub_right {R : Type x} [NonUnitalNonAssocRing R] {a : R} {b : R} {c : R} :

Commute a b → Commute a c → Commute a (b - c)

source

@[simp]

theorem Commute.sub_left {R : Type x} [NonUnitalNonAssocRing R] {a : R} {b : R} {c : R} :

Commute a c → Commute b c → Commute (a - b) c

source

theorem mul_self_sub_mul_self {R : Type x} [CommRing R] (a : R) (b : R) :

a * a - b * b = (a + b) * (a - b)

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

source

theorem mul_self_sub_one {R : Type x} [NonAssocRing R] (a : R) :

a * a - 1 = (a + 1) * (a - 1)

source

theorem mul_self_eq_mul_self_iff {R : Type x} [CommRing R] [NoZeroDivisors R] {a : R} {b : R} :

a * a = b * b ↔ a = b ∨ a = -b

source

theorem mul_self_eq_one_iff {R : Type x} [NonAssocRing R] [NoZeroDivisors R] {a : R} :

a * a = 1 ↔ a = 1 ∨ a = -1

source

theorem Units.inv_eq_self_iff {R : Type x} [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.