mathlib documentation

algebra.ring.defs

Semirings and rings #

THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.

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 #

Tags #

semiring, comm_semiring, ring, comm_ring, domain, is_domain, nonzero, units

distrib class #

@[instance]
def distrib.to_has_mul (R : Type u_1) [self : distrib R] :
@[class]
structure distrib (R : Type u_1) :
Type u_1
  • mul : R R R
  • add : R R R
  • left_distrib : (a b c : R), a * (b + c) = a * b + a * c
  • 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 of this typeclass
Instances of other typeclasses for distrib
  • distrib.has_sizeof_inst
@[instance]
def distrib.to_has_add (R : Type u_1) [self : distrib R] :
@[class]
structure left_distrib_class (R : Type u_1) [has_mul R] [has_add R] :
  • left_distrib : (a b c : R), a * (b + c) = a * b + a * c

A typeclass stating that multiplication is left distributive over addition.

Instances of this typeclass
Instances of other typeclasses for left_distrib_class
  • left_distrib_class.has_sizeof_inst
@[class]
structure right_distrib_class (R : Type u_1) [has_mul R] [has_add R] :
  • right_distrib : (a b c : R), (a + b) * c = a * c + b * c

A typeclass stating that multiplication is right distributive over addition.

Instances of this typeclass
Instances of other typeclasses for right_distrib_class
  • right_distrib_class.has_sizeof_inst
@[protected, instance]
Equations
@[protected, instance]
Equations
theorem left_distrib {R : Type x} [has_mul R] [has_add R] [left_distrib_class R] (a b c : R) :
a * (b + c) = a * b + a * c
theorem mul_add {R : Type x} [has_mul R] [has_add R] [left_distrib_class R] (a b c : R) :
a * (b + c) = a * b + a * c

Alias of left_distrib.

theorem right_distrib {R : Type x} [has_mul R] [has_add R] [right_distrib_class R] (a b c : R) :
(a + b) * c = a * c + b * c
theorem add_mul {R : Type x} [has_mul R] [has_add R] [right_distrib_class R] (a b c : R) :
(a + b) * c = a * c + b * c

Alias of right_distrib.

theorem distrib_three_right {R : Type x} [has_mul R] [has_add R] [right_distrib_class R] (a b c d : R) :
(a + b + c) * d = a * d + b * d + c * d

Semirings #

@[class]
structure non_unital_non_assoc_semiring (α : Type u) :

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

Instances of this typeclass
Instances of other typeclasses for non_unital_non_assoc_semiring
  • non_unital_non_assoc_semiring.has_sizeof_inst
@[class]
structure non_unital_semiring (α : Type u) :

An associative but not-necessarily unital semiring.

Instances of this typeclass
Instances of other typeclasses for non_unital_semiring
  • non_unital_semiring.has_sizeof_inst
@[class]
structure non_assoc_semiring (α : Type u) :

A unital but not-necessarily-associative semiring.

Instances of this typeclass
Instances of other typeclasses for non_assoc_semiring
  • non_assoc_semiring.has_sizeof_inst
@[instance]
@[class]
structure semiring (α : Type u) :

A semiring is a type with the following structures: additive commutative monoid (add_comm_monoid), multiplicative monoid (monoid), distributive laws (distrib), and multiplication by zero law (mul_zero_class). The actual definition extends monoid_with_zero instead of monoid and mul_zero_class.

Instances of this typeclass
Instances of other typeclasses for semiring
  • semiring.has_sizeof_inst
@[instance]
@[instance]
theorem one_add_one_eq_two {α : Type u} [has_one α] [has_add α] :
1 + 1 = 2
theorem add_one_mul {α : Type u} [has_add α] [mul_one_class α] [right_distrib_class α] (a b : α) :
(a + 1) * b = a * b + b
theorem mul_add_one {α : Type u} [has_add α] [mul_one_class α] [left_distrib_class α] (a b : α) :
a * (b + 1) = a * b + a
theorem one_add_mul {α : Type u} [has_add α] [mul_one_class α] [right_distrib_class α] (a b : α) :
(1 + a) * b = b + a * b
theorem mul_one_add {α : Type u} [has_add α] [mul_one_class α] [left_distrib_class α] (a b : α) :
a * (1 + b) = a + a * b
theorem two_mul {α : Type u} [has_add α] [mul_one_class α] [right_distrib_class α] (n : α) :
2 * n = n + n
theorem bit0_eq_two_mul {α : Type u} [has_add α] [mul_one_class α] [right_distrib_class α] (n : α) :
bit0 n = 2 * n
theorem mul_two {α : Type u} [has_add α] [mul_one_class α] [left_distrib_class α] (n : α) :
n * 2 = n + n
theorem add_ite {α : Type u_1} [has_add α] (P : Prop) [decidable P] (a b c : α) :
a + ite P b c = ite P (a + b) (a + c)
@[simp]
theorem mul_ite {α : Type u_1} [has_mul α] (P : Prop) [decidable P] (a b c : α) :
a * ite P b c = ite P (a * b) (a * c)
theorem ite_add {α : Type u_1} [has_add α] (P : Prop) [decidable P] (a b c : α) :
ite P a b + c = ite P (a + c) (b + c)
@[simp]
theorem ite_mul {α : Type u_1} [has_mul α] (P : Prop) [decidable P] (a b c : α) :
ite P a b * c = ite P (a * c) (b * c)
@[simp]
theorem mul_boole {α : Type u_1} [mul_zero_one_class α] (P : Prop) [decidable P] (a : α) :
a * ite P 1 0 = ite P a 0
@[simp]
theorem boole_mul {α : Type u_1} [mul_zero_one_class α] (P : Prop) [decidable P] (a : α) :
ite P 1 0 * a = ite P a 0
theorem ite_mul_zero_left {α : Type u_1} [mul_zero_class α] (P : Prop) [decidable P] (a b : α) :
ite P (a * b) 0 = ite P a 0 * b
theorem ite_mul_zero_right {α : Type u_1} [mul_zero_class α] (P : Prop) [decidable P] (a b : α) :
ite P (a * b) 0 = a * ite P b 0
theorem ite_and_mul_zero {α : Type u_1} [mul_zero_class α] (P Q : Prop) [decidable P] [decidable Q] (a b : α) :
ite (P Q) (a * b) 0 = ite P a 0 * ite Q b 0
@[class]
structure non_unital_comm_semiring (α : Type u) :

A non-unital commutative semiring is a non_unital_semiring with commutative multiplication. In other words, it is a type with the following structures: additive commutative monoid (add_comm_monoid), commutative semigroup (comm_semigroup), distributive laws (distrib), and multiplication by zero law (mul_zero_class).

Instances of this typeclass
Instances of other typeclasses for non_unital_comm_semiring
  • non_unital_comm_semiring.has_sizeof_inst
@[class]
structure comm_semiring (α : Type u) :

A commutative semiring is a semiring with commutative multiplication. In other words, it is a type with the following structures: additive commutative monoid (add_comm_monoid), multiplicative commutative monoid (comm_monoid), distributive laws (distrib), and multiplication by zero law (mul_zero_class).

Instances of this typeclass
Instances of other typeclasses for comm_semiring
  • comm_semiring.has_sizeof_inst
@[instance]
theorem add_mul_self_eq {α : Type u} [comm_semiring α] (a b : α) :
(a + b) * (a + b) = a * a + 2 * a * b + b * b
@[class]
structure has_distrib_neg (α : Type u_1) [has_mul α] :
Type u_1
  • neg : α α
  • neg_neg : (x : α), --x = x
  • neg_mul : (x y : α), -x * y = -(x * y)
  • 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 of this typeclass
Instances of other typeclasses for has_distrib_neg
  • has_distrib_neg.has_sizeof_inst
@[simp]
theorem neg_mul {α : Type u} [has_mul α] [has_distrib_neg α] (a b : α) :
-a * b = -(a * b)
@[simp]
theorem mul_neg {α : Type u} [has_mul α] [has_distrib_neg α] (a b : α) :
a * -b = -(a * b)
theorem neg_mul_neg {α : Type u} [has_mul α] [has_distrib_neg α] (a b : α) :
-a * -b = a * b
theorem neg_mul_eq_neg_mul {α : Type u} [has_mul α] [has_distrib_neg α] (a b : α) :
-(a * b) = -a * b
theorem neg_mul_eq_mul_neg {α : Type u} [has_mul α] [has_distrib_neg α] (a b : α) :
-(a * b) = a * -b
theorem neg_mul_comm {α : Type u} [has_mul α] [has_distrib_neg α] (a b : α) :
-a * b = a * -b
theorem neg_eq_neg_one_mul {α : Type u} [mul_one_class α] [has_distrib_neg α] (a : α) :
-a = (-1) * a
theorem mul_neg_one {α : Type u} [mul_one_class α] [has_distrib_neg α] (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} [mul_one_class α] [has_distrib_neg α] (a : α) :
(-1) * a = -a

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

Rings #

@[class]
structure non_unital_non_assoc_ring (α : Type u) :

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

Instances of this typeclass
Instances of other typeclasses for non_unital_non_assoc_ring
  • non_unital_non_assoc_ring.has_sizeof_inst
@[class]
structure non_unital_ring (α : Type u_1) :
Type u_1

An associative but not-necessarily unital ring.

Instances of this typeclass
Instances of other typeclasses for non_unital_ring
  • non_unital_ring.has_sizeof_inst
@[class]
structure non_assoc_ring (α : Type u_1) :
Type u_1

A unital but not-necessarily-associative ring.

Instances of this typeclass
Instances of other typeclasses for non_assoc_ring
  • non_assoc_ring.has_sizeof_inst
@[instance]
def ring.to_monoid (α : Type u) [self : ring α] :
@[instance]
@[class]
structure ring (α : Type u) :

A ring is a type with the following structures: additive commutative group (add_comm_group), multiplicative monoid (monoid), and distributive laws (distrib). Equivalently, a ring is a semiring with a negation operation making it an additive group.

Instances of this typeclass
Instances of other typeclasses for ring
  • ring.has_sizeof_inst
@[instance]
def ring.to_distrib (α : Type u) [self : ring α] :
theorem mul_sub_left_distrib {α : Type u} [non_unital_non_assoc_ring α] (a b c : α) :
a * (b - c) = a * b - a * c
theorem mul_sub {α : Type u} [non_unital_non_assoc_ring α] (a b c : α) :
a * (b - c) = a * b - a * c

Alias of mul_sub_left_distrib.

theorem mul_sub_right_distrib {α : Type u} [non_unital_non_assoc_ring α] (a b c : α) :
(a - b) * c = a * c - b * c
theorem sub_mul {α : Type u} [non_unital_non_assoc_ring α] (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} [non_unital_non_assoc_ring α] {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} [non_unital_non_assoc_ring α] {a b c d e : α} :
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} [non_assoc_ring α] (a b : α) :
(a - 1) * b = a * b - b
theorem mul_sub_one {α : Type u} [non_assoc_ring α] (a b : α) :
a * (b - 1) = a * b - a
theorem one_sub_mul {α : Type u} [non_assoc_ring α] (a b : α) :
(1 - a) * b = b - a * b
theorem mul_one_sub {α : Type u} [non_assoc_ring α] (a b : α) :
a * (1 - b) = a - a * b
@[protected, instance]
Equations
@[protected, instance]
Equations
@[protected, instance]
def ring.to_semiring {α : Type u} [ring α] :
Equations
Instances for ring.to_semiring
@[class]
structure non_unital_comm_ring (α : Type u) :

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

Instances of this typeclass
Instances of other typeclasses for non_unital_comm_ring
  • non_unital_comm_ring.has_sizeof_inst
@[instance]
def comm_ring.to_ring (α : Type u) [self : comm_ring α] :
ring α
Instances for comm_ring.to_ring
@[class]
structure comm_ring (α : Type u) :

A commutative ring is a ring with commutative multiplication.

Instances of this typeclass
Instances of other typeclasses for comm_ring
  • comm_ring.has_sizeof_inst
@[instance]
def comm_ring.to_comm_monoid (α : Type u) [self : comm_ring α] :
@[instance]
@[class]
structure is_domain (α : Type u) [semiring α] :
Prop
  • mul_left_cancel_of_ne_zero : {a b c : α}, a 0 a * b = a * c b = c
  • mul_right_cancel_of_ne_zero : {a b c : α}, b 0 a * b = c * b a = c
  • exists_pair_ne : (x y : α), x y

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 and ∀ {a b c : R}, b ≠ 0 → a * b = c * b → a = c.

This is implemented as a mixin for semiring α. To obtain an integral domain use [comm_ring α] [is_domain α].

Instances of this typeclass
@[instance]
def is_domain.to_nontrivial (α : Type u) [semiring α] [self : is_domain α] :