mathlib3 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 #

source
@[instance]
def distrib.to_has_mul (R : Type u_1) [self : distrib R] :
has_mul R
source
@[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
source
@[instance]
def distrib.to_has_add (R : Type u_1) [self : distrib R] :
has_add R
source
@[class]
structure left_distrib_class (R : Type u_1) [has_mul R] [has_add R] :
Type
  • 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
source
@[class]
structure right_distrib_class (R : Type u_1) [has_mul R] [has_add R] :
Type
  • 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
source
@[protected, instance]
def distrib.left_distrib_class (R : Type u_1) [distrib R] :
left_distrib_class R
Equations
source
@[protected, instance]
def distrib.right_distrib_class (R : Type u_1) [distrib R] :
right_distrib_class R
Equations
source
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
source
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.

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

source
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 #

source
@[instance]
def non_unital_non_assoc_semiring.to_distrib (α : Type u) [self : non_unital_non_assoc_semiring α] :
distrib α
source
@[instance]
def non_unital_non_assoc_semiring.to_mul_zero_class (α : Type u) [self : non_unital_non_assoc_semiring α] :
mul_zero_class α
source
@[instance]
def non_unital_non_assoc_semiring.to_add_comm_monoid (α : Type u) [self : non_unital_non_assoc_semiring α] :
add_comm_monoid α
source
@[class]
structure non_unital_non_assoc_semiring (α : Type u) :
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
source
@[instance]
def non_unital_semiring.to_semigroup_with_zero (α : Type u) [self : non_unital_semiring α] :
semigroup_with_zero α
source
@[instance]
def non_unital_semiring.to_non_unital_non_assoc_semiring (α : Type u) [self : non_unital_semiring α] :
non_unital_non_assoc_semiring α
source
@[class]
structure non_unital_semiring (α : Type u) :
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
source
@[instance]
def non_assoc_semiring.to_non_unital_non_assoc_semiring (α : Type u) [self : non_assoc_semiring α] :
non_unital_non_assoc_semiring α
source
@[instance]
def non_assoc_semiring.to_mul_zero_one_class (α : Type u) [self : non_assoc_semiring α] :
mul_zero_one_class α
source
@[instance]
def non_assoc_semiring.to_add_comm_monoid_with_one (α : Type u) [self : non_assoc_semiring α] :
add_comm_monoid_with_one α
source
@[class]
structure non_assoc_semiring (α : Type u) :
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
source
@[instance]
def semiring.to_non_assoc_semiring (α : Type u) [self : semiring α] :
non_assoc_semiring α
source
@[class]
structure semiring (α : Type u) :
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
source
@[instance]
def semiring.to_non_unital_semiring (α : Type u) [self : semiring α] :
non_unital_semiring α
source
@[instance]
def semiring.to_monoid_with_zero (α : Type u) [self : semiring α] :
monoid_with_zero α
source
theorem one_add_one_eq_two {α : Type u} [has_one α] [has_add α] :
1 + 1 = 2
source
theorem add_one_mul {α : Type u} [has_add α] [mul_one_class α] [right_distrib_class α] (a b : α) :
(a + 1) * b = a * b + b
source
theorem mul_add_one {α : Type u} [has_add α] [mul_one_class α] [left_distrib_class α] (a b : α) :
a * (b + 1) = a * b + a
source
theorem one_add_mul {α : Type u} [has_add α] [mul_one_class α] [right_distrib_class α] (a b : α) :
(1 + a) * b = b + a * b
source
theorem mul_one_add {α : Type u} [has_add α] [mul_one_class α] [left_distrib_class α] (a b : α) :
a * (1 + b) = a + a * b
source
theorem two_mul {α : Type u} [has_add α] [mul_one_class α] [right_distrib_class α] (n : α) :
2 * n = n + n
source
theorem bit0_eq_two_mul {α : Type u} [has_add α] [mul_one_class α] [right_distrib_class α] (n : α) :
bit0 n = 2 * n
source
theorem mul_two {α : Type u} [has_add α] [mul_one_class α] [left_distrib_class α] (n : α) :
n * 2 = n + n
source
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)
source
@[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)
source
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)
source
@[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)
source
@[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
source
@[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
source
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
source
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
source
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
source
@[class]
structure non_unital_comm_semiring (α : Type u) :
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
source
@[instance]
def non_unital_comm_semiring.to_comm_semigroup (α : Type u) [self : non_unital_comm_semiring α] :
comm_semigroup α
source
@[instance]
def non_unital_comm_semiring.to_non_unital_semiring (α : Type u) [self : non_unital_comm_semiring α] :
non_unital_semiring α
source
@[class]
structure comm_semiring (α : Type u) :
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
source
@[instance]
def comm_semiring.to_comm_monoid (α : Type u) [self : comm_semiring α] :
comm_monoid α
source
@[instance]
def comm_semiring.to_semiring (α : Type u) [self : comm_semiring α] :
semiring α
Instances for comm_semiring.to_semiring
source
@[protected, instance]
def comm_semiring.to_non_unital_comm_semiring {α : Type u} [comm_semiring α] :
non_unital_comm_semiring α
Equations
source
@[protected, instance]
def comm_semiring.to_comm_monoid_with_zero {α : Type u} [comm_semiring α] :
comm_monoid_with_zero α
Equations
source
theorem add_mul_self_eq {α : Type u} [comm_semiring α] (a b : α) :
(a + b) * (a + b) = a * a + 2 * a * b + b * b
source
@[instance]
def has_distrib_neg.to_has_involutive_neg (α : Type u_1) [has_mul α] [self : has_distrib_neg α] :
has_involutive_neg α
source
@[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
source
@[simp]
theorem neg_mul {α : Type u} [has_mul α] [has_distrib_neg α] (a b : α) :
-a * b = -(a * b)
source
@[simp]
theorem mul_neg {α : Type u} [has_mul α] [has_distrib_neg α] (a b : α) :
a * -b = -(a * b)
source
theorem neg_mul_neg {α : Type u} [has_mul α] [has_distrib_neg α] (a b : α) :
-a * -b = a * b
source
theorem neg_mul_eq_neg_mul {α : Type u} [has_mul α] [has_distrib_neg α] (a b : α) :
-(a * b) = -a * b
source
theorem neg_mul_eq_mul_neg {α : Type u} [has_mul α] [has_distrib_neg α] (a b : α) :
-(a * b) = a * -b
source
theorem neg_mul_comm {α : Type u} [has_mul α] [has_distrib_neg α] (a b : α) :
-a * b = a * -b
source
theorem neg_eq_neg_one_mul {α : Type u} [mul_one_class α] [has_distrib_neg α] (a : α) :
-a = (-1) * a
source
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.

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

source
@[protected, instance]
def mul_zero_class.neg_zero_class {α : Type u} [mul_zero_class α] [has_distrib_neg α] :
neg_zero_class α
Equations

Rings #

source
@[instance]
def non_unital_non_assoc_ring.to_non_unital_non_assoc_semiring (α : Type u) [self : non_unital_non_assoc_ring α] :
non_unital_non_assoc_semiring α
source
@[class]
structure non_unital_non_assoc_ring (α : Type u) :
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
source
@[instance]
def non_unital_non_assoc_ring.to_add_comm_group (α : Type u) [self : non_unital_non_assoc_ring α] :
add_comm_group α
source
@[instance]
def non_unital_ring.to_non_unital_semiring (α : Type u_1) [self : non_unital_ring α] :
non_unital_semiring α
source
@[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
source
@[instance]
def non_unital_ring.to_non_unital_non_assoc_ring (α : Type u_1) [self : non_unital_ring α] :
non_unital_non_assoc_ring α
source
@[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
source
@[instance]
def non_assoc_ring.to_add_comm_group_with_one (α : Type u_1) [self : non_assoc_ring α] :
add_comm_group_with_one α
source
@[instance]
def non_assoc_ring.to_non_assoc_semiring (α : Type u_1) [self : non_assoc_ring α] :
non_assoc_semiring α
source
@[instance]
def non_assoc_ring.to_non_unital_non_assoc_ring (α : Type u_1) [self : non_assoc_ring α] :
non_unital_non_assoc_ring α
source
@[instance]
def ring.to_monoid (α : Type u) [self : ring α] :
monoid α
source
@[instance]
def ring.to_add_comm_group_with_one (α : Type u) [self : ring α] :
add_comm_group_with_one α
source
@[class]
structure ring (α : Type u) :
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
source
@[instance]
def ring.to_distrib (α : Type u) [self : ring α] :
distrib α
source
@[protected, instance]
def non_unital_non_assoc_ring.to_has_distrib_neg {α : Type u} [non_unital_non_assoc_ring α] :
has_distrib_neg α
Equations
source
theorem mul_sub_left_distrib {α : Type u} [non_unital_non_assoc_ring α] (a b c : α) :
a * (b - c) = a * b - a * c
source
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.

source
theorem mul_sub_right_distrib {α : Type u} [non_unital_non_assoc_ring α] (a b c : α) :
(a - b) * c = a * c - b * c
source
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.

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

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

source
theorem sub_one_mul {α : Type u} [non_assoc_ring α] (a b : α) :
(a - 1) * b = a * b - b
source
theorem mul_sub_one {α : Type u} [non_assoc_ring α] (a b : α) :
a * (b - 1) = a * b - a
source
theorem one_sub_mul {α : Type u} [non_assoc_ring α] (a b : α) :
(1 - a) * b = b - a * b
source
theorem mul_one_sub {α : Type u} [non_assoc_ring α] (a b : α) :
a * (1 - b) = a - a * b
source
@[protected, instance]
def ring.to_non_unital_ring {α : Type u} [ring α] :
non_unital_ring α
Equations
source
@[protected, instance]
def ring.to_non_assoc_ring {α : Type u} [ring α] :
non_assoc_ring α
Equations
source
@[protected, instance]
def ring.to_semiring {α : Type u} [ring α] :
semiring α
Equations
Instances for ring.to_semiring
source
@[class]
structure non_unital_comm_ring (α : Type u) :
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
source
@[instance]
def non_unital_comm_ring.to_comm_semigroup (α : Type u) [self : non_unital_comm_ring α] :
comm_semigroup α
source
@[instance]
def non_unital_comm_ring.to_non_unital_ring (α : Type u) [self : non_unital_comm_ring α] :
non_unital_ring α
source
@[protected, instance]
def non_unital_comm_ring.to_non_unital_comm_semiring {α : Type u} [s : non_unital_comm_ring α] :
non_unital_comm_semiring α
Equations
source
@[instance]
def comm_ring.to_ring (α : Type u) [self : comm_ring α] :
ring α
Instances for comm_ring.to_ring
source
@[class]
structure comm_ring (α : Type u) :
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
source
@[instance]
def comm_ring.to_comm_monoid (α : Type u) [self : comm_ring α] :
comm_monoid α
source
@[protected, instance]
def comm_ring.to_comm_semiring {α : Type u} [s : comm_ring α] :
comm_semiring α
Equations
source
@[protected, instance]
def comm_ring.to_non_unital_comm_ring {α : Type u} [s : comm_ring α] :
non_unital_comm_ring α
Equations
source
@[instance]
def is_domain.to_is_cancel_mul_zero (α : Type u) [semiring α] [self : is_domain α] :
is_cancel_mul_zero α
source
@[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
source
@[instance]
def is_domain.to_nontrivial (α : Type u) [semiring α] [self : is_domain α] :
nontrivial α