# Documentation

Mathlib.Algebra.Ring.Defs

# Semirings and rings #

This file defines semirings, rings and domains. This is analogous to Algebra.Group.Defs and Algebra.Group.Basic, the difference being that the former is about + and * separately, while the present file is about their interaction.

## Main definitions #

• Distrib: Typeclass for distributivity of multiplication over addition.
• HasDistribNeg: Typeclass for commutativity of negation and multiplication. This is useful when dealing with multiplicative submonoids which are closed under negation without being closed under addition, for example units.
• (NonUnital_)(NonAssoc_)(Semi)ring: Typeclasses for possibly non-unital or non-associative rings and semirings. Some combinations are not defined yet because they haven't found use.

## Tags #

Semiring, CommSemiring, Ring, CommRing, domain, IsDomain, nonzero, units

### distrib class #

class Distrib (R : Type u_1) extends , :
Type u_1
• Multiplication is left distributive over addition

left_distrib : ∀ (a b c : R), a * (b + c) = a * b + a * c
• Multiplication is right distributive over addition

right_distrib : ∀ (a b c : R), (a + b) * c = a * c + b * c

A typeclass stating that multiplication is left and right distributive over addition.

Instances
class LeftDistribClass (R : Type u_1) [inst : Mul R] [inst : Add R] :
• Multiplication is left distributive over addition

left_distrib : ∀ (a b c : R), a * (b + c) = a * b + a * c

A typeclass stating that multiplication is left distributive over addition.

Instances
class RightDistribClass (R : Type u_1) [inst : Mul R] [inst : Add R] :
• Multiplication is right distributive over addition

right_distrib : ∀ (a b c : R), (a + b) * c = a * c + b * c

A typeclass stating that multiplication is right distributive over addition.

Instances
instance Distrib.leftDistribClass (R : Type u_1) [inst : ] :
Equations
• = { left_distrib := (_ : ∀ (a b c : R), a * (b + c) = a * b + a * c) }
instance Distrib.rightDistribClass (R : Type u_1) [inst : ] :
Equations
• = { right_distrib := (_ : ∀ (a b c : R), (a + b) * c = a * c + b * c) }
theorem left_distrib {R : Type x} [inst : Mul R] [inst : Add R] [inst : ] (a : R) (b : R) (c : R) :
a * (b + c) = a * b + a * c
theorem mul_add {R : Type x} [inst : Mul R] [inst : Add R] [inst : ] (a : R) (b : R) (c : R) :
a * (b + c) = a * b + a * c

Alias of left_distrib.

theorem right_distrib {R : Type x} [inst : Mul R] [inst : Add R] [inst : ] (a : R) (b : R) (c : R) :
(a + b) * c = a * c + b * c
theorem add_mul {R : Type x} [inst : Mul R] [inst : Add R] [inst : ] (a : R) (b : R) (c : R) :
(a + b) * c = a * c + b * c

Alias of right_distrib.

theorem distrib_three_right {R : Type x} [inst : Mul R] [inst : Add R] [inst : ] (a : R) (b : R) (c : R) (d : R) :
(a + b + c) * d = a * d + b * d + c * d

### Semirings #

class NonUnitalNonAssocSemiring (α : Type u) extends , :
• Multiplication is left distributive over addition

left_distrib : ∀ (a b c : α), a * (b + c) = a * b + a * c
• Multiplication is right distributive over addition

right_distrib : ∀ (a b c : α), (a + b) * c = a * c + b * c
• Zero is a left absorbing element for multiplication

zero_mul : ∀ (a : α), 0 * a = 0
• Zero is a right absorbing element for multiplication

mul_zero : ∀ (a : α), a * 0 = 0

A not-necessarily-unital, not-necessarily-associative semiring.

Instances
class NonUnitalSemiring (α : Type u) extends :
• Multiplication is associative

mul_assoc : ∀ (a b c : α), a * b * c = a * (b * c)

An associative but not-necessarily unital semiring.

Instances
class NonAssocSemiring (α : Type u) extends , , :
• One is a right neutral element for multiplication

mul_one : ∀ (a : α), a * 1 = a
• toNatCast :
• The canonical map ℕ → R→ R sends 0 : ℕ to 0 : R.

natCast_zero :
• The canonical map ℕ → R→ R is a homomorphism.

natCast_succ : autoParam (∀ (n : ), NatCast.natCast (n + 1) = ) _auto✝

A unital but not-necessarily-associative semiring.

Instances
class Semiring (α : Type u) extends , , :
• One is a right neutral element for multiplication

mul_one : ∀ (a : α), a * 1 = a
• toNatCast :
• The canonical map ℕ → R→ R sends 0 : ℕ to 0 : R.

natCast_zero :
• The canonical map ℕ → R→ R is a homomorphism.

natCast_succ : autoParam (∀ (n : ), NatCast.natCast (n + 1) = ) _auto✝
• Raising to the power of a natural number.

npow : αα
• Raising to the power (0 : ℕ) gives 1.

npow_zero : autoParam (∀ (x : α), npow 0 x = 1) _auto✝
• Raising to the power (n + 1 : ℕ) behaves as expected.

npow_succ : autoParam (∀ (n : ) (x : α), npow (n + 1) x = x * npow n x) _auto✝
Instances
theorem add_one_mul {α : Type u} [inst : Add α] [inst : ] [inst : ] (a : α) (b : α) :
(a + 1) * b = a * b + b
theorem mul_add_one {α : Type u} [inst : Add α] [inst : ] [inst : ] (a : α) (b : α) :
a * (b + 1) = a * b + a
theorem one_add_mul {α : Type u} [inst : Add α] [inst : ] [inst : ] (a : α) (b : α) :
(1 + a) * b = b + a * b
theorem mul_one_add {α : Type u} [inst : Add α] [inst : ] [inst : ] (a : α) (b : α) :
a * (1 + b) = a + a * b
theorem two_mul {α : Type u} [inst : ] (n : α) :
2 * n = n + n
theorem bit0_eq_two_mul {α : Type u} [inst : ] (n : α) :
bit0 n = 2 * n
theorem mul_two {α : Type u} [inst : ] (n : α) :
n * 2 = n + n
theorem add_ite {α : Type u_1} [inst : Add α] (P : Prop) [inst : ] (a : α) (b : α) (c : α) :
(a + if P then b else c) = if P then a + b else a + c
@[simp]
theorem mul_ite {α : Type u_1} [inst : Mul α] (P : Prop) [inst : ] (a : α) (b : α) (c : α) :
(a * if P then b else c) = if P then a * b else a * c
theorem ite_add {α : Type u_1} [inst : Add α] (P : Prop) [inst : ] (a : α) (b : α) (c : α) :
(if P then a else b) + c = if P then a + c else b + c
@[simp]
theorem ite_mul {α : Type u_1} [inst : Mul α] (P : Prop) [inst : ] (a : α) (b : α) (c : α) :
(if P then a else b) * c = if P then a * c else b * c
theorem mul_boole {α : Type u_1} [inst : ] (P : Prop) [inst : ] (a : α) :
(a * if P then 1 else 0) = if P then a else 0
theorem boole_mul {α : Type u_1} [inst : ] (P : Prop) [inst : ] (a : α) :
(if P then 1 else 0) * a = if P then a else 0
theorem ite_mul_zero_left {α : Type u_1} [inst : ] (P : Prop) [inst : ] (a : α) (b : α) :
(if P then a * b else 0) = (if P then a else 0) * b
theorem ite_mul_zero_right {α : Type u_1} [inst : ] (P : Prop) [inst : ] (a : α) (b : α) :
(if P then a * b else 0) = a * if P then b else 0
theorem ite_and_mul_zero {α : Type u_1} [inst : ] (P : Prop) (Q : Prop) [inst : ] [inst : ] (a : α) (b : α) :
(if P Q then a * b else 0) = (if P then a else 0) * if Q then b else 0
class NonUnitalCommSemiring (α : Type u) extends :
• Multiplication is commutative in a commutative semigroup.

mul_comm : ∀ (a b : α), a * b = b * a

A non-unital commutative semiring is a NonUnitalSemiring with commutative multiplication. In other words, it is a type with the following structures: additive commutative monoid (AddCommMonoid), commutative semigroup (CommSemigroup), distributive laws (Distrib), and multiplication by zero law (MulZeroClass).

Instances
class CommSemiring (R : Type u) extends :
• Multiplication is commutative in a commutative semigroup.

mul_comm : ∀ (a b : R), a * b = b * a
Instances
instance CommSemiring.toNonUnitalCommSemiring {α : Type u} [inst : ] :
Equations
instance CommSemiring.toCommMonoidWithZero {α : Type u} [inst : ] :
Equations
• One or more equations did not get rendered due to their size.
theorem add_mul_self_eq {α : Type u} [inst : ] (a : α) (b : α) :
(a + b) * (a + b) = a * a + 2 * a * b + b * b
class HasDistribNeg (α : Type u_1) [inst : Mul α] extends :
Type u_1
• Negation is left distributive over multiplication

neg_mul : ∀ (x y : α), -x * y = -(x * y)
• Negation is right distributive over multiplication

mul_neg : ∀ (x y : α), x * -y = -(x * y)

Typeclass for a negation operator that distributes across multiplication.

This is useful for dealing with submonoids of a ring that contain -1 without having to duplicate lemmas.

Instances
@[simp]
theorem neg_mul {α : Type u} [inst : Mul α] [inst : ] (a : α) (b : α) :
-a * b = -(a * b)
@[simp]
theorem mul_neg {α : Type u} [inst : Mul α] [inst : ] (a : α) (b : α) :
a * -b = -(a * b)
theorem neg_mul_neg {α : Type u} [inst : Mul α] [inst : ] (a : α) (b : α) :
-a * -b = a * b
theorem neg_mul_eq_neg_mul {α : Type u} [inst : Mul α] [inst : ] (a : α) (b : α) :
-(a * b) = -a * b
theorem neg_mul_eq_mul_neg {α : Type u} [inst : Mul α] [inst : ] (a : α) (b : α) :
-(a * b) = a * -b
theorem neg_mul_comm {α : Type u} [inst : Mul α] [inst : ] (a : α) (b : α) :
-a * b = a * -b
theorem neg_eq_neg_one_mul {α : Type u} [inst : ] [inst : ] (a : α) :
-a = -1 * a
theorem mul_neg_one {α : Type u} [inst : ] [inst : ] (a : α) :
a * -1 = -a

An element of a ring multiplied by the additive inverse of one is the element's additive inverse.

theorem neg_one_mul {α : Type u} [inst : ] [inst : ] (a : α) :
-1 * a = -a

The additive inverse of one multiplied by an element of a ring is the element's additive inverse.

instance MulZeroClass.negZeroClass {α : Type u} [inst : ] [inst : ] :
Equations

### Rings #

class NonUnitalNonAssocRing (α : Type u) extends , :
• Multiplication is left distributive over addition

left_distrib : ∀ (a b c : α), a * (b + c) = a * b + a * c
• Multiplication is right distributive over addition

right_distrib : ∀ (a b c : α), (a + b) * c = a * c + b * c
• Zero is a left absorbing element for multiplication

zero_mul : ∀ (a : α), 0 * a = 0
• Zero is a right absorbing element for multiplication

mul_zero : ∀ (a : α), a * 0 = 0

A not-necessarily-unital, not-necessarily-associative ring.

Instances
class NonUnitalRing (α : Type u_1) extends :
Type u_1
• Multiplication is associative

mul_assoc : ∀ (a b c : α), a * b * c = a * (b * c)

An associative but not-necessarily unital ring.

Instances
class NonAssocRing (α : Type u_1) extends , , , :
Type u_1
• toNatCast :
• The canonical map ℕ → R→ R sends 0 : ℕ to 0 : R.

natCast_zero :
• The canonical map ℕ → R→ R is a homomorphism.

natCast_succ : autoParam (∀ (n : ), NatCast.natCast (n + 1) = ) _auto✝
• toIntCast :
• The canonical homorphism ℤ → R→ R agrees with the one from ℕ → R→ R on ℕ.

intCast_ofNat : autoParam (∀ (n : ), = n) _auto✝
• The canonical homorphism ℤ → R→ R for negative values is just the negation of the values of the canonical homomorphism ℕ → R→ R.

intCast_negSucc : autoParam (∀ (n : ), = -↑(n + 1)) _auto✝

A unital but not-necessarily-associative ring.

Instances
class Ring (R : Type u) extends , , , :
• zsmul : RR
• zsmul_zero' : autoParam (∀ (a : R), zsmul 0 a = 0) _auto✝
• zsmul_succ' : autoParam (∀ (n : ) (a : R), zsmul () a = a + zsmul () a) _auto✝
• zsmul_neg' : autoParam (∀ (n : ) (a : R), zsmul () a = -zsmul (↑()) a) _auto✝
• add_left_neg : ∀ (a : R), -a + a = 0
• toIntCast :
• The canonical homorphism ℤ → R→ R agrees with the one from ℕ → R→ R on ℕ.

intCast_ofNat : autoParam (∀ (n : ), = n) _auto✝
• The canonical homorphism ℤ → R→ R for negative values is just the negation of the values of the canonical homomorphism ℕ → R→ R.

intCast_negSucc : autoParam (∀ (n : ), = -↑(n + 1)) _auto✝
Instances
instance NonUnitalNonAssocRing.toHasDistribNeg {α : Type u} [inst : ] :
Equations
• NonUnitalNonAssocRing.toHasDistribNeg = HasDistribNeg.mk (_ : ∀ (a b : α), -a * b = -(a * b)) (_ : ∀ (a b : α), a * -b = -(a * b))
theorem mul_sub_left_distrib {α : Type u} [inst : ] (a : α) (b : α) (c : α) :
a * (b - c) = a * b - a * c
theorem mul_sub {α : Type u} [inst : ] (a : α) (b : α) (c : α) :
a * (b - c) = a * b - a * c

Alias of mul_sub_left_distrib.

theorem mul_sub_right_distrib {α : Type u} [inst : ] (a : α) (b : α) (c : α) :
(a - b) * c = a * c - b * c
theorem sub_mul {α : Type u} [inst : ] (a : α) (b : α) (c : α) :
(a - b) * c = a * c - b * c

Alias of mul_sub_right_distrib.

theorem mul_add_eq_mul_add_iff_sub_mul_add_eq {α : Type u} [inst : ] {a : α} {b : α} {c : α} {d : α} {e : α} :
a * e + c = b * e + d (a - b) * e + c = d

An iff statement following from right distributivity in rings and the definition of subtraction.

theorem sub_mul_add_eq_of_mul_add_eq_mul_add {α : Type u} [inst : ] {a : α} {b : α} {c : α} {d : α} {e : α} (h : a * e + c = b * e + d) :
(a - b) * e + c = d

A simplification of one side of an equation exploiting right distributivity in rings and the definition of subtraction.

theorem sub_one_mul {α : Type u} [inst : ] (a : α) (b : α) :
(a - 1) * b = a * b - b
theorem mul_sub_one {α : Type u} [inst : ] (a : α) (b : α) :
a * (b - 1) = a * b - a
theorem one_sub_mul {α : Type u} [inst : ] (a : α) (b : α) :
(1 - a) * b = b - a * b
theorem mul_one_sub {α : Type u} [inst : ] (a : α) (b : α) :
a * (1 - b) = a - a * b
instance Ring.toNonUnitalRing {α : Type u} [inst : Ring α] :
Equations
instance Ring.toNonAssocRing {α : Type u} [inst : Ring α] :
Equations
• Ring.toNonAssocRing = let src := inst; NonAssocRing.mk (_ : ∀ (a : α), 1 * a = a) (_ : ∀ (a : α), a * 1 = a)
instance instSemiring {α : Type u} [inst : Ring α] :
Equations
• instSemiring = let src := inst; Semiring.mk (_ : ∀ (a : α), 1 * a = a) (_ : ∀ (a : α), a * 1 = a) Semiring.npow
class NonUnitalCommRing (α : Type u) extends :
• Multiplication is commutative in a commutative semigroup.

mul_comm : ∀ (a b : α), a * b = b * a

A non-unital commutative ring is a NonUnitalRing with commutative multiplication.

Instances
Equations
class CommRing (α : Type u) extends :
• Multiplication is commutative in a commutative semigroup.

mul_comm : ∀ (a b : α), a * b = b * a
Instances
instance CommRing.toCommSemiring {α : Type u} [s : ] :
Equations
instance CommRing.toNonUnitalCommRing {α : Type u} [s : ] :
Equations
instance CommRing.toAddCommGroupWithOne {α : Type u} [s : ] :
Equations
A domain is a nontrivial semiring such multiplication by a non zero element is cancellative, on both sides. In other words, a nontrivial semiring R satisfying ∀ {a b c : R}, a ≠ 0 → a * b = a * c → b = c∀ {a b c : R}, a ≠ 0 → a * b = a * c → b = c≠ 0 → a * b = a * c → b = c→ a * b = a * c → b = c→ b = c and ∀ {a b c : R}, b ≠ 0 → a * b = c * b → a = c∀ {a b c : R}, b ≠ 0 → a * b = c * b → a = c≠ 0 → a * b = c * b → a = c→ a * b = c * b → a = c→ a = c.
This is implemented as a mixin for Semiring α. To obtain an integral domain use [CommRing α] [IsDomain α].