# mathlibdocumentation

algebra.ring.basic

# 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.
• `has_distrib_neg`: 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`.
• `(non_unital_)(non_assoc_)(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`, `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] :
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
@[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
@[protected, instance]
def distrib.left_distrib_class (R : Type u_1) [distrib R] :
Equations
@[protected, instance]
def distrib.right_distrib_class (R : Type u_1) [distrib R] :
Equations
theorem left_distrib {R : Type x} [has_mul R] [has_add R] (a b c : R) :
a * (b + c) = a * b + a * c
theorem mul_add {R : Type x} [has_mul R] [has_add 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] (a b c : R) :
(a + b) * c = a * c + b * c
theorem add_mul {R : Type x} [has_mul R] [has_add 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] (a b c d : R) :
(a + b + c) * d = a * d + b * d + c * d
@[protected, reducible]
def function.injective.distrib {R : Type x} {S : Type u_1} [has_mul R] [has_add R] [distrib S] (f : R → S) (hf : function.injective f) (add : ∀ (x y : R), f (x + y) = f x + f y) (mul : ∀ (x y : R), f (x * y) = f x * f y) :

Pullback a `distrib` instance along an injective function. See note [reducible non-instances].

Equations
@[protected, reducible]
def function.surjective.distrib {R : Type x} {S : Type u_1} [distrib R] [has_add S] [has_mul S] (f : R → S) (hf : function.surjective f) (add : ∀ (x y : R), f (x + y) = f x + f y) (mul : ∀ (x y : R), f (x * y) = f x * f y) :

Pushforward a `distrib` instance along a surjective function. See note [reducible non-instances].

Equations

### Semirings #

@[class]
structure non_unital_non_assoc_semiring (α : Type u) :
Type u
• add : α → α → α
• add_assoc : ∀ (a b c : α), a + b + c = a + (b + c)
• zero : α
• zero_add : ∀ (a : α), 0 + a = a
• add_zero : ∀ (a : α), a + 0 = a
• nsmul : α → α
• nsmul_zero' : (∀ (x : α), . "try_refl_tac"
• nsmul_succ' : (∀ (n : ) (x : α), . "try_refl_tac"
• add_comm : ∀ (a b : α), a + b = b + a
• mul : α → α → α
• left_distrib : ∀ (a b c : α), a * (b + c) = a * b + a * c
• right_distrib : ∀ (a b c : α), (a + b) * c = a * c + b * c
• zero_mul : ∀ (a : α), 0 * a = 0
• mul_zero : ∀ (a : α), a * 0 = 0

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
@[instance]
@[class]
structure non_unital_semiring (α : Type u) :
Type u
• add : α → α → α
• add_assoc : ∀ (a b c : α), a + b + c = a + (b + c)
• zero : α
• zero_add : ∀ (a : α), 0 + a = a
• add_zero : ∀ (a : α), a + 0 = a
• nsmul : α → α
• nsmul_zero' : (∀ (x : α), . "try_refl_tac"
• nsmul_succ' : (∀ (n : ) (x : α), . "try_refl_tac"
• add_comm : ∀ (a b : α), a + b = b + a
• mul : α → α → α
• left_distrib : ∀ (a b c : α), a * (b + c) = a * b + a * c
• right_distrib : ∀ (a b c : α), (a + b) * c = a * c + b * c
• zero_mul : ∀ (a : α), 0 * a = 0
• mul_zero : ∀ (a : α), a * 0 = 0
• mul_assoc : ∀ (a b c : α), a * b * c = a * (b * c)

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
@[instance]
@[instance]
@[class]
structure non_assoc_semiring (α : Type u) :
Type u
• add : α → α → α
• add_assoc : ∀ (a b c : α), a + b + c = a + (b + c)
• zero : α
• zero_add : ∀ (a : α), 0 + a = a
• add_zero : ∀ (a : α), a + 0 = a
• nsmul : α → α
• nsmul_zero' : (∀ (x : α), . "try_refl_tac"
• nsmul_succ' : (∀ (n : ) (x : α), . "try_refl_tac"
• add_comm : ∀ (a b : α), a + b = b + a
• mul : α → α → α
• left_distrib : ∀ (a b c : α), a * (b + c) = a * b + a * c
• right_distrib : ∀ (a b c : α), (a + b) * c = a * c + b * c
• zero_mul : ∀ (a : α), 0 * a = 0
• mul_zero : ∀ (a : α), a * 0 = 0
• one : α
• one_mul : ∀ (a : α), 1 * a = a
• mul_one : ∀ (a : α), a * 1 = a
• nat_cast : → α
• nat_cast_zero : . "control_laws_tac"
• nat_cast_succ : (∀ (n : ), . "control_laws_tac"

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]
def semiring.to_non_assoc_semiring (α : Type u) [self : semiring α] :
@[class]
structure semiring (α : Type u) :
Type u
• add : α → α → α
• add_assoc : ∀ (a b c : α), a + b + c = a + (b + c)
• zero : α
• zero_add : ∀ (a : α), 0 + a = a
• add_zero : ∀ (a : α), a + 0 = a
• nsmul : α → α
• nsmul_zero' : (∀ (x : α), = 0) . "try_refl_tac"
• nsmul_succ' : (∀ (n : ) (x : α), = x + x) . "try_refl_tac"
• add_comm : ∀ (a b : α), a + b = b + a
• mul : α → α → α
• left_distrib : ∀ (a b c : α), a * (b + c) = a * b + a * c
• right_distrib : ∀ (a b c : α), (a + b) * c = a * c + b * c
• zero_mul : ∀ (a : α), 0 * a = 0
• mul_zero : ∀ (a : α), a * 0 = 0
• mul_assoc : ∀ (a b c : α), a * b * c = a * (b * c)
• one : α
• one_mul : ∀ (a : α), 1 * a = a
• mul_one : ∀ (a : α), a * 1 = a
• nat_cast : → α
• nat_cast_zero : . "control_laws_tac"
• nat_cast_succ : (∀ (n : ), semiring.nat_cast (n + 1) = . "control_laws_tac"
• npow : α → α
• npow_zero' : (∀ (x : α), = 1) . "try_refl_tac"
• npow_succ' : (∀ (n : ) (x : α), = x * x) . "try_refl_tac"

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]
def semiring.to_non_unital_semiring (α : Type u) [self : semiring α] :
@[instance]
def semiring.to_monoid_with_zero (α : Type u) [self : semiring α] :
@[protected, reducible]
def function.injective.non_unital_non_assoc_semiring {β : Type v} [has_zero β] [has_add β] [has_mul β] [ β] {α : Type u} (f : β → α) (hf : function.injective f) (zero : f 0 = 0) (add : ∀ (x y : β), f (x + y) = f x + f y) (mul : ∀ (x y : β), f (x * y) = f x * f y) (nsmul : ∀ (x : β) (n : ), f (n x) = n f x) :

Pullback a `non_unital_non_assoc_semiring` instance along an injective function. See note [reducible non-instances].

Equations
@[protected, reducible]
def function.injective.non_unital_semiring {β : Type v} [has_zero β] [has_add β] [has_mul β] [ β] {α : Type u} (f : β → α) (hf : function.injective f) (zero : f 0 = 0) (add : ∀ (x y : β), f (x + y) = f x + f y) (mul : ∀ (x y : β), f (x * y) = f x * f y) (nsmul : ∀ (x : β) (n : ), f (n x) = n f x) :

Pullback a `non_unital_semiring` instance along an injective function. See note [reducible non-instances].

Equations
@[protected, reducible]
def function.injective.non_assoc_semiring {α : Type u} {β : Type v} [has_zero β] [has_one β] [has_mul β] [has_add β] [ β] [has_nat_cast β] (f : β → α) (hf : function.injective f) (zero : f 0 = 0) (one : f 1 = 1) (add : ∀ (x y : β), f (x + y) = f x + f y) (mul : ∀ (x y : β), f (x * y) = f x * f y) (nsmul : ∀ (x : β) (n : ), f (n x) = n f x) (nat_cast : ∀ (n : ), f n = n) :

Pullback a `non_assoc_semiring` instance along an injective function. See note [reducible non-instances].

Equations
@[protected, reducible]
def function.injective.semiring {α : Type u} [semiring α] {β : Type v} [has_zero β] [has_one β] [has_add β] [has_mul β] [ ] [ β] [has_nat_cast β] (f : β → α) (hf : function.injective f) (zero : f 0 = 0) (one : f 1 = 1) (add : ∀ (x y : β), f (x + y) = f x + f y) (mul : ∀ (x y : β), f (x * y) = f x * f y) (nsmul : ∀ (x : β) (n : ), f (n x) = n f x) (npow : ∀ (x : β) (n : ), f (x ^ n) = f x ^ n) (nat_cast : ∀ (n : ), f n = n) :

Pullback a `semiring` instance along an injective function. See note [reducible non-instances].

Equations
@[protected, reducible]
def function.surjective.non_unital_non_assoc_semiring {β : Type v} [has_zero β] [has_add β] [has_mul β] [ β] {α : Type u} (f : α → β) (hf : function.surjective f) (zero : f 0 = 0) (add : ∀ (x y : α), f (x + y) = f x + f y) (mul : ∀ (x y : α), f (x * y) = f x * f y) (nsmul : ∀ (x : α) (n : ), f (n x) = n f x) :

Pushforward a `non_unital_non_assoc_semiring` instance along a surjective function. See note [reducible non-instances].

Equations
@[protected, reducible]
def function.surjective.non_unital_semiring {β : Type v} [has_zero β] [has_add β] [has_mul β] [ β] {α : Type u} (f : α → β) (hf : function.surjective f) (zero : f 0 = 0) (add : ∀ (x y : α), f (x + y) = f x + f y) (mul : ∀ (x y : α), f (x * y) = f x * f y) (nsmul : ∀ (x : α) (n : ), f (n x) = n f x) :

Pushforward a `non_unital_semiring` instance along a surjective function. See note [reducible non-instances].

Equations
@[protected, reducible]
def function.surjective.non_assoc_semiring {α : Type u} {β : Type v} [has_zero β] [has_one β] [has_add β] [has_mul β] [ β] [has_nat_cast β] (f : α → β) (hf : function.surjective f) (zero : f 0 = 0) (one : f 1 = 1) (add : ∀ (x y : α), f (x + y) = f x + f y) (mul : ∀ (x y : α), f (x * y) = f x * f y) (nsmul : ∀ (x : α) (n : ), f (n x) = n f x) (nat_cast : ∀ (n : ), f n = n) :

Pushforward a `non_assoc_semiring` instance along a surjective function. See note [reducible non-instances].

Equations
@[protected, reducible]
def function.surjective.semiring {α : Type u} [semiring α] {β : Type v} [has_zero β] [has_one β] [has_add β] [has_mul β] [ ] [ β] [has_nat_cast β] (f : α → β) (hf : function.surjective f) (zero : f 0 = 0) (one : f 1 = 1) (add : ∀ (x y : α), f (x + y) = f x + f y) (mul : ∀ (x y : α), f (x * y) = f x * f y) (nsmul : ∀ (x : α) (n : ), f (n x) = n f x) (npow : ∀ (x : α) (n : ), f (x ^ n) = f x ^ n) (nat_cast : ∀ (n : ), f n = n) :

Pushforward a `semiring` instance along a surjective function. See note [reducible non-instances].

Equations
1 + 1 = 2
theorem dvd_add {α : Type u} [has_add α] [semigroup α] {a b c : α} (h₁ : a b) (h₂ : a c) :
a b + c
theorem add_one_mul {α : Type u} [has_add α] (a b : α) :
(a + 1) * b = a * b + b
theorem mul_add_one {α : Type u} [has_add α] (a b : α) :
a * (b + 1) = a * b + a
theorem one_add_mul {α : Type u} [has_add α] (a b : α) :
(1 + a) * b = b + a * b
theorem mul_one_add {α : Type u} [has_add α] (a b : α) :
a * (1 + b) = a + a * b
theorem two_mul {α : Type u} [has_add α] (n : α) :
2 * n = n + n
theorem bit0_eq_two_mul {α : Type u} [has_add α] (n : α) :
bit0 n = 2 * n
theorem mul_two {α : Type u} [has_add α] (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} (P : Prop) [decidable P] (a : α) :
a * ite P 1 0 = ite P a 0
@[simp]
theorem boole_mul {α : Type u_1} (P : Prop) [decidable P] (a : α) :
ite P 1 0 * a = ite P a 0
theorem ite_mul_zero_left {α : Type u_1} (P : Prop) [decidable P] (a b : α) :
ite P (a * b) 0 = ite P a 0 * b
theorem ite_mul_zero_right {α : Type u_1} (P : Prop) [decidable P] (a b : α) :
ite P (a * b) 0 = a * ite P b 0
theorem ite_and_mul_zero {α : Type u_1} (P Q : Prop) [decidable P] [decidable Q] (a b : α) :
ite (P Q) (a * b) 0 = ite P a 0 * ite Q b 0
def add_hom.mul_left {R : Type u_1} [distrib R] (r : R) :
R

Left multiplication by an element of a type with distributive multiplication is an `add_hom`.

Equations
@[simp]
theorem add_hom.mul_left_apply {R : Type u_1} [distrib R] (r : R) :
@[simp]
theorem add_hom.mul_right_apply {R : Type u_1} [distrib R] (r : R) :
= λ (a : R), a * r
def add_hom.mul_right {R : Type u_1} [distrib R] (r : R) :
R

Left multiplication by an element of a type with distributive multiplication is an `add_hom`.

Equations
@[simp]
theorem map_bit0 {α : Type u} {β : Type v} {F : Type u_1} [ β] (f : F) (a : α) :
f (bit0 a) = bit0 (f a)

Additive homomorphisms preserve `bit0`.

def add_monoid_hom.mul_left {R : Type u_1} (r : R) :
R →+ R

Left multiplication by an element of a (semi)ring is an `add_monoid_hom`

Equations
@[simp]
theorem add_monoid_hom.coe_mul_left {R : Type u_1} (r : R) :
def add_monoid_hom.mul_right {R : Type u_1} (r : R) :
R →+ R

Right multiplication by an element of a (semi)ring is an `add_monoid_hom`

Equations
@[simp]
theorem add_monoid_hom.coe_mul_right {R : Type u_1} (r : R) :
= λ (_x : R), _x * r
theorem add_monoid_hom.mul_right_apply {R : Type u_1} (a r : R) :
= a * r
@[simp]
theorem two_dvd_bit0 {α : Type u} [semiring α] {a : α} :
2 bit0 a
@[class]
structure non_unital_comm_semiring (α : Type u) :
Type u
• add : α → α → α
• add_assoc : ∀ (a b c : α), a + b + c = a + (b + c)
• zero : α
• zero_add : ∀ (a : α), 0 + a = a
• add_zero : ∀ (a : α), a + 0 = a
• nsmul : α → α
• nsmul_zero' : (∀ (x : α), . "try_refl_tac"
• nsmul_succ' : (∀ (n : ) (x : α), . "try_refl_tac"
• add_comm : ∀ (a b : α), a + b = b + a
• mul : α → α → α
• left_distrib : ∀ (a b c : α), a * (b + c) = a * b + a * c
• right_distrib : ∀ (a b c : α), (a + b) * c = a * c + b * c
• zero_mul : ∀ (a : α), 0 * a = 0
• mul_zero : ∀ (a : α), a * 0 = 0
• mul_assoc : ∀ (a b c : α), a * b * c = a * (b * c)
• mul_comm : ∀ (a b : α), a * b = b * a

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
@[instance]
@[protected, reducible]
def function.injective.non_unital_comm_semiring {α : Type u} {γ : Type w} [has_zero γ] [has_add γ] [has_mul γ] [ γ] (f : γ → α) (hf : function.injective f) (zero : f 0 = 0) (add : ∀ (x y : γ), f (x + y) = f x + f y) (mul : ∀ (x y : γ), f (x * y) = f x * f y) (nsmul : ∀ (x : γ) (n : ), f (n x) = n f x) :

Pullback a `non_unital_semiring` instance along an injective function. See note [reducible non-instances].

Equations
@[protected, reducible]
def function.surjective.non_unital_comm_semiring {α : Type u} {γ : Type w} [has_zero γ] [has_add γ] [has_mul γ] [ γ] (f : α → γ) (hf : function.surjective f) (zero : f 0 = 0) (add : ∀ (x y : α), f (x + y) = f x + f y) (mul : ∀ (x y : α), f (x * y) = f x * f y) (nsmul : ∀ (x : α) (n : ), f (n x) = n f x) :

Pushforward a `non_unital_semiring` instance along a surjective function. See note [reducible non-instances].

Equations
theorem has_dvd.dvd.linear_comb {α : Type u} {d x y : α} (hdx : d x) (hdy : d y) (a b : α) :
d a * x + b * y
@[class]
structure comm_semiring (α : Type u) :
Type u
• add : α → α → α
• add_assoc : ∀ (a b c : α), a + b + c = a + (b + c)
• zero : α
• zero_add : ∀ (a : α), 0 + a = a
• add_zero : ∀ (a : α), a + 0 = a
• nsmul : α → α
• nsmul_zero' : (∀ (x : α), = 0) . "try_refl_tac"
• nsmul_succ' : (∀ (n : ) (x : α), = x + . "try_refl_tac"
• add_comm : ∀ (a b : α), a + b = b + a
• mul : α → α → α
• left_distrib : ∀ (a b c : α), a * (b + c) = a * b + a * c
• right_distrib : ∀ (a b c : α), (a + b) * c = a * c + b * c
• zero_mul : ∀ (a : α), 0 * a = 0
• mul_zero : ∀ (a : α), a * 0 = 0
• mul_assoc : ∀ (a b c : α), a * b * c = a * (b * c)
• one : α
• one_mul : ∀ (a : α), 1 * a = a
• mul_one : ∀ (a : α), a * 1 = a
• nat_cast : → α
• nat_cast_zero : . "control_laws_tac"
• nat_cast_succ : (∀ (n : ), comm_semiring.nat_cast (n + 1) = . "control_laws_tac"
• npow : α → α
• npow_zero' : (∀ (x : α), = 1) . "try_refl_tac"
• npow_succ' : (∀ (n : ) (x : α), = x * . "try_refl_tac"
• mul_comm : ∀ (a b : α), a * b = b * a

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]
def comm_semiring.to_comm_monoid (α : Type u) [self : comm_semiring α] :
@[instance]
def comm_semiring.to_semiring (α : Type u) [self : comm_semiring α] :
Instances for `comm_semiring.to_semiring`
@[protected, instance]
Equations
@[protected, instance]
Equations
@[protected, reducible]
def function.injective.comm_semiring {α : Type u} {γ : Type w} [has_zero γ] [has_one γ] [has_add γ] [has_mul γ] [ γ] [has_nat_cast γ] [ ] (f : γ → α) (hf : function.injective f) (zero : f 0 = 0) (one : f 1 = 1) (add : ∀ (x y : γ), f (x + y) = f x + f y) (mul : ∀ (x y : γ), f (x * y) = f x * f y) (nsmul : ∀ (x : γ) (n : ), f (n x) = n f x) (npow : ∀ (x : γ) (n : ), f (x ^ n) = f x ^ n) (nat_cast : ∀ (n : ), f n = n) :

Pullback a `semiring` instance along an injective function. See note [reducible non-instances].

Equations
@[protected, reducible]
def function.surjective.comm_semiring {α : Type u} {γ : Type w} [has_zero γ] [has_one γ] [has_add γ] [has_mul γ] [ γ] [has_nat_cast γ] [ ] (f : α → γ) (hf : function.surjective f) (zero : f 0 = 0) (one : f 1 = 1) (add : ∀ (x y : α), f (x + y) = f x + f y) (mul : ∀ (x y : α), f (x * y) = f x * f y) (nsmul : ∀ (x : α) (n : ), f (n x) = n f x) (npow : ∀ (x : α) (n : ), f (x ^ n) = f x ^ n) (nat_cast : ∀ (n : ), f n = n) :

Pushforward a `semiring` instance along a surjective function. See note [reducible non-instances].

Equations
theorem add_mul_self_eq {α : Type u} (a b : α) :
(a + b) * (a + b) = a * a + 2 * a * b + b * b
@[instance]
def has_distrib_neg.to_has_involutive_neg (α : Type u_1) [has_mul α] [self : has_distrib_neg α] :
@[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 α] (a b : α) :
-a * b = -(a * b)
@[simp]
theorem mul_neg {α : Type u} [has_mul α] (a b : α) :
a * -b = -(a * b)
theorem neg_mul_neg {α : Type u} [has_mul α] (a b : α) :
-a * -b = a * b
theorem neg_mul_eq_neg_mul {α : Type u} [has_mul α] (a b : α) :
-(a * b) = -a * b
theorem neg_mul_eq_mul_neg {α : Type u} [has_mul α] (a b : α) :
-(a * b) = a * -b
theorem neg_mul_comm {α : Type u} [has_mul α] (a b : α) :
-a * b = a * -b
@[protected, reducible]
def function.injective.has_distrib_neg {α : Type u} {β : Type v} [has_mul α] [has_neg β] [has_mul β] (f : β → α) (hf : function.injective f) (neg : ∀ (a : β), f (-a) = -f a) (mul : ∀ (a b : β), f (a * b) = f a * f b) :

A type endowed with `-` and `*` has distributive negation, if it admits an injective map that preserves `-` and `*` to a type which has distributive negation.

Equations
@[protected, reducible]
def function.surjective.has_distrib_neg {α : Type u} {β : Type v} [has_mul α] [has_neg β] [has_mul β] (f : α → β) (hf : function.surjective f) (neg : ∀ (a : α), f (-a) = -f a) (mul : ∀ (a b : α), f (a * b) = f a * f b) :

A type endowed with `-` and `*` has distributive negation, if it admits a surjective map that preserves `-` and `*` from a type which has distributive negation.

Equations
@[protected, instance]
def add_opposite.has_distrib_neg {α : Type u} [has_mul α]  :
Equations
@[protected, instance]
def mul_opposite.has_distrib_neg {α : Type u} [has_mul α]  :
Equations
theorem neg_eq_neg_one_mul {α : Type u} (a : α) :
-a = (-1) * a
theorem mul_neg_one {α : Type u} (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} (a : α) :
(-1) * a = -a

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

@[simp]
theorem neg_zero' {α : Type u}  :
-0 = 0

Prefer `neg_zero` if `subtraction_monoid` is available.

theorem dvd_neg_of_dvd {α : Type u} [semigroup α] {a b : α} (h : a b) :
a -b
theorem dvd_of_dvd_neg {α : Type u} [semigroup α] {a b : α} (h : a -b) :
a b
@[simp]
theorem dvd_neg {α : Type u} [semigroup α] (a b : α) :
a -b a b

An element a of a semigroup with a distributive negation divides the negation of an element b iff a divides b.

theorem neg_dvd_of_dvd {α : Type u} [semigroup α] {a b : α} (h : a b) :
-a b
theorem dvd_of_neg_dvd {α : Type u} [semigroup α] {a b : α} (h : -a b) :
a b
@[simp]
theorem neg_dvd {α : Type u} [semigroup α] (a b : α) :
-a b a b

The negation of an element a of a semigroup with a distributive negation divides another element b iff a divides b.

@[simp]
theorem inv_neg' {α : Type u} [group α] (a : α) :

### Rings #

@[class]
structure non_unital_non_assoc_ring (α : Type u) :
Type u
• add : α → α → α
• add_assoc : ∀ (a b c : α), a + b + c = a + (b + c)
• zero : α
• zero_add : ∀ (a : α), 0 + a = a
• add_zero : ∀ (a : α), a + 0 = a
• nsmul : α → α
• nsmul_zero' : (∀ (x : α), . "try_refl_tac"
• nsmul_succ' : (∀ (n : ) (x : α), . "try_refl_tac"
• neg : α → α
• sub : α → α → α
• sub_eq_add_neg : (∀ (a b : α), a - b = a + -b) . "try_refl_tac"
• zsmul : α → α
• zsmul_zero' : (∀ (a : α), . "try_refl_tac"
• zsmul_succ' : (∀ (n : ) (a : α), . "try_refl_tac"
• zsmul_neg' : (∀ (n : ) (a : α), . "try_refl_tac"
• add_left_neg : ∀ (a : α), -a + a = 0
• add_comm : ∀ (a b : α), a + b = b + a
• mul : α → α → α
• left_distrib : ∀ (a b c : α), a * (b + c) = a * b + a * c
• right_distrib : ∀ (a b c : α), (a + b) * c = a * c + b * c
• zero_mul : ∀ (a : α), 0 * a = 0
• mul_zero : ∀ (a : α), a * 0 = 0

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
@[protected, reducible]
def function.injective.non_unital_non_assoc_ring {α : Type u} {β : Type v} [has_zero β] [has_add β] [has_mul β] [has_neg β] [has_sub β] [ β] [ β] (f : β → α) (hf : function.injective f) (zero : f 0 = 0) (add : ∀ (x y : β), f (x + y) = f x + f y) (mul : ∀ (x y : β), f (x * y) = f x * f y) (neg : ∀ (x : β), f (-x) = -f x) (sub : ∀ (x y : β), f (x - y) = f x - f y) (nsmul : ∀ (x : β) (n : ), f (n x) = n f x) (zsmul : ∀ (x : β) (n : ), f (n x) = n f x) :

Pullback a `non_unital_non_assoc_ring` instance along an injective function. See note [reducible non-instances].

Equations
@[protected, reducible]
def function.surjective.non_unital_non_assoc_ring {α : Type u} {β : Type v} [has_zero β] [has_add β] [has_mul β] [has_neg β] [has_sub β] [ β] [ β] (f : α → β) (hf : function.surjective f) (zero : f 0 = 0) (add : ∀ (x y : α), f (x + y) = f x + f y) (mul : ∀ (x y : α), f (x * y) = f x * f y) (neg : ∀ (x : α), f (-x) = -f x) (sub : ∀ (x y : α), f (x - y) = f x - f y) (nsmul : ∀ (x : α) (n : ), f (n x) = n f x) (zsmul : ∀ (x : α) (n : ), f (n x) = n f x) :

Pushforward a `non_unital_non_assoc_ring` instance along a surjective function. See note [reducible non-instances].

Equations
@[protected, instance]
Equations
theorem mul_sub_left_distrib {α : Type u} (a b c : α) :
a * (b - c) = a * b - a * c
theorem mul_sub {α : Type u} (a b c : α) :
a * (b - c) = a * b - a * c

Alias of `mul_sub_left_distrib`.

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

Alias of `mul_sub_right_distrib`.

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.

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.

@[instance]
def non_unital_ring.to_non_unital_semiring (α : Type u_1) [self : non_unital_ring α] :
@[class]
structure non_unital_ring (α : Type u_1) :
Type u_1
• add : α → α → α
• add_assoc : ∀ (a b c : α), a + b + c = a + (b + c)
• zero : α
• zero_add : ∀ (a : α), 0 + a = a
• add_zero : ∀ (a : α), a + 0 = a
• nsmul : α → α
• nsmul_zero' : (∀ (x : α), = 0) . "try_refl_tac"
• nsmul_succ' : (∀ (n : ) (x : α), = x + . "try_refl_tac"
• neg : α → α
• sub : α → α → α
• sub_eq_add_neg : (∀ (a b : α), a - b = a + -b) . "try_refl_tac"
• zsmul : α → α
• zsmul_zero' : (∀ (a : α), = 0) . "try_refl_tac"
• zsmul_succ' : (∀ (n : ) (a : α), = a + . "try_refl_tac"
• zsmul_neg' : (∀ (n : ) (a : α), . "try_refl_tac"
• add_left_neg : ∀ (a : α), -a + a = 0
• add_comm : ∀ (a b : α), a + b = b + a
• mul : α → α → α
• left_distrib : ∀ (a b c : α), a * (b + c) = a * b + a * c
• right_distrib : ∀ (a b c : α), (a + b) * c = a * c + b * c
• zero_mul : ∀ (a : α), 0 * a = 0
• mul_zero : ∀ (a : α), a * 0 = 0
• mul_assoc : ∀ (a b c : α), a * b * c = a * (b * c)

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
@[instance]
@[protected, reducible]
def function.injective.non_unital_ring {α : Type u} {β : Type v} [has_zero β] [has_add β] [has_mul β] [has_neg β] [has_sub β] [ β] [ β] (f : β → α) (hf : function.injective f) (zero : f 0 = 0) (add : ∀ (x y : β), f (x + y) = f x + f y) (mul : ∀ (x y : β), f (x * y) = f x * f y) (neg : ∀ (x : β), f (-x) = -f x) (sub : ∀ (x y : β), f (x - y) = f x - f y) (nsmul : ∀ (x : β) (n : ), f (n x) = n f x) (gsmul : ∀ (x : β) (n : ), f (n x) = n f x) :

Pullback a `non_unital_ring` instance along an injective function. See note [reducible non-instances].

Equations
@[protected, reducible]
def function.surjective.non_unital_ring {α : Type u} {β : Type v} [has_zero β] [has_add β] [has_mul β] [has_neg β] [has_sub β] [ β] [ β] (f : α → β) (hf : function.surjective f) (zero : f 0 = 0) (add : ∀ (x y : α), f (x + y) = f x + f y) (mul : ∀ (x y : α), f (x * y) = f x * f y) (neg : ∀ (x : α), f (-x) = -f x) (sub : ∀ (x y : α), f (x - y) = f x - f y) (nsmul : ∀ (x : α) (n : ), f (n x) = n f x) (gsmul : ∀ (x : α) (n : ), f (n x) = n f x) :

Pushforward a `non_unital_ring` instance along a surjective function. See note [reducible non-instances].

Equations
@[class]
structure non_assoc_ring (α : Type u_1) :
Type u_1
• add : α → α → α
• add_assoc : ∀ (a b c : α), a + b + c = a + (b + c)
• zero : α
• zero_add : ∀ (a : α), 0 + a = a
• add_zero : ∀ (a : α), a + 0 = a
• nsmul : α → α
• nsmul_zero' : (∀ (x : α), = 0) . "try_refl_tac"
• nsmul_succ' : (∀ (n : ) (x : α), = x + . "try_refl_tac"
• neg : α → α
• sub : α → α → α
• sub_eq_add_neg : (∀ (a b : α), a - b = a + -b) . "try_refl_tac"
• zsmul : α → α
• zsmul_zero' : (∀ (a : α), = 0) . "try_refl_tac"
• zsmul_succ' : (∀ (n : ) (a : α), = a + . "try_refl_tac"
• zsmul_neg' : (∀ (n : ) (a : α), = - a) . "try_refl_tac"
• add_left_neg : ∀ (a : α), -a + a = 0
• add_comm : ∀ (a b : α), a + b = b + a
• mul : α → α → α
• left_distrib : ∀ (a b c : α), a * (b + c) = a * b + a * c
• right_distrib : ∀ (a b c : α), (a + b) * c = a * c + b * c
• zero_mul : ∀ (a : α), 0 * a = 0
• mul_zero : ∀ (a : α), a * 0 = 0
• one : α
• one_mul : ∀ (a : α), 1 * a = a
• mul_one : ∀ (a : α), a * 1 = a
• nat_cast : → α
• nat_cast_zero : . "control_laws_tac"
• nat_cast_succ : (∀ (n : ), non_assoc_ring.nat_cast (n + 1) = . "control_laws_tac"
• int_cast : → α
• int_cast_of_nat : (∀ (n : ), . "control_laws_tac"
• int_cast_neg_succ_of_nat : (∀ (n : ), non_assoc_ring.int_cast (-(n + 1)) = -(n + 1)) . "control_laws_tac"

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 non_assoc_ring.to_add_group_with_one (α : Type u_1) [self : non_assoc_ring α] :
@[instance]
def non_assoc_ring.to_non_assoc_semiring (α : Type u_1) [self : non_assoc_ring α] :
@[instance]
def non_assoc_ring.to_non_unital_non_assoc_ring (α : Type u_1) [self : non_assoc_ring α] :
@[protected, reducible]
def function.injective.non_assoc_ring {α : Type u} {β : Type v} [has_zero β] [has_one β] [has_add β] [has_mul β] [has_neg β] [has_sub β] [ β] [ β] [has_nat_cast β] [has_int_cast β] (f : β → α) (hf : function.injective f) (zero : f 0 = 0) (one : f 1 = 1) (add : ∀ (x y : β), f (x + y) = f x + f y) (mul : ∀ (x y : β), f (x * y) = f x * f y) (neg : ∀ (x : β), f (-x) = -f x) (sub : ∀ (x y : β), f (x - y) = f x - f y) (nsmul : ∀ (x : β) (n : ), f (n x) = n f x) (gsmul : ∀ (x : β) (n : ), f (n x) = n f x) (nat_cast : ∀ (n : ), f n = n) (int_cast : ∀ (n : ), f n = n) :

Pullback a `non_assoc_ring` instance along an injective function. See note [reducible non-instances].

Equations
@[protected, reducible]
def function.surjective.non_assoc_ring {α : Type u} {β : Type v} [has_zero β] [has_one β] [has_add β] [has_mul β] [has_neg β] [has_sub β] [ β] [ β] [has_nat_cast β] [has_int_cast β] (f : α → β) (hf : function.surjective f) (zero : f 0 = 0) (one : f 1 = 1) (add : ∀ (x y : α), f (x + y) = f x + f y) (mul : ∀ (x y : α), f (x * y) = f x * f y) (neg : ∀ (x : α), f (-x) = -f x) (sub : ∀ (x y : α), f (x - y) = f x - f y) (nsmul : ∀ (x : α) (n : ), f (n x) = n f x) (gsmul : ∀ (x : α) (n : ), f (n x) = n f x) (nat_cast : ∀ (n : ), f n = n) (int_cast : ∀ (n : ), f n = n) :

Pushforward a `non_unital_ring` instance along a surjective function. See note [reducible non-instances].

Equations
theorem sub_one_mul {α : Type u} (a b : α) :
(a - 1) * b = a * b - b
theorem mul_sub_one {α : Type u} (a b : α) :
a * (b - 1) = a * b - a
theorem one_sub_mul {α : Type u} (a b : α) :
(1 - a) * b = b - a * b
theorem mul_one_sub {α : Type u} (a b : α) :
a * (1 - b) = a - a * b
@[instance]
def ring.to_monoid (α : Type u) [self : ring α] :
@[instance]
def ring.to_add_comm_group_with_one (α : Type u) [self : ring α] :
@[class]
structure ring (α : Type u) :
Type u
• add : α → α → α
• add_assoc : ∀ (a b c : α), a + b + c = a + (b + c)
• zero : α
• zero_add : ∀ (a : α), 0 + a = a
• add_zero : ∀ (a : α), a + 0 = a
• nsmul : α → α
• nsmul_zero' : (∀ (x : α), x = 0) . "try_refl_tac"
• nsmul_succ' : (∀ (n : ) (x : α), x = x + x) . "try_refl_tac"
• neg : α → α
• sub : α → α → α
• sub_eq_add_neg : (∀ (a b : α), a - b = a + -b) . "try_refl_tac"
• zsmul : α → α
• zsmul_zero' : (∀ (a : α), a = 0) . "try_refl_tac"
• zsmul_succ' : (∀ (n : ) (a : α), a = a + a) . "try_refl_tac"
• zsmul_neg' : (∀ (n : ) (a : α), a = -ring.zsmul (n.succ) a) . "try_refl_tac"
• add_left_neg : ∀ (a : α), -a + a = 0
• add_comm : ∀ (a b : α), a + b = b + a
• int_cast : → α
• nat_cast : → α
• one : α
• nat_cast_zero : . "control_laws_tac"
• nat_cast_succ : (∀ (n : ), ring.nat_cast (n + 1) = + 1) . "control_laws_tac"
• int_cast_of_nat : (∀ (n : ), = n) . "control_laws_tac"
• int_cast_neg_succ_of_nat : (∀ (n : ), ring.int_cast (-(n + 1)) = -(n + 1)) . "control_laws_tac"
• mul : α → α → α
• mul_assoc : ∀ (a b c : α), a * b * c = a * (b * c)
• one_mul : ∀ (a : α), 1 * a = a
• mul_one : ∀ (a : α), a * 1 = a
• npow : α → α
• npow_zero' : (∀ (x : α), x = 1) . "try_refl_tac"
• npow_succ' : (∀ (n : ) (x : α), x = x * x) . "try_refl_tac"
• left_distrib : ∀ (a b c : α), a * (b + c) = a * b + a * c
• right_distrib : ∀ (a b c : α), (a + b) * c = a * c + b * c

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 α] :
@[protected, instance]
def ring.to_non_unital_ring {α : Type u} [ring α] :
Equations
@[protected, instance]
def ring.to_non_assoc_ring {α : Type u} [ring α] :
Equations
@[protected, instance]
def ring.to_semiring {α : Type u} [ring α] :
Equations
Instances for `ring.to_semiring`
@[protected, reducible]
def function.injective.ring {α : Type u} {β : Type v} [ring α] [has_zero β] [has_one β] [has_add β] [has_mul β] [has_neg β] [has_sub β] [ β] [ β] [ ] [has_nat_cast β] [has_int_cast β] (f : β → α) (hf : function.injective f) (zero : f 0 = 0) (one : f 1 = 1) (add : ∀ (x y : β), f (x + y) = f x + f y) (mul : ∀ (x y : β), f (x * y) = f x * f y) (neg : ∀ (x : β), f (-x) = -f x) (sub : ∀ (x y : β), f (x - y) = f x - f y) (nsmul : ∀ (x : β) (n : ), f (n x) = n f x) (zsmul : ∀ (x : β) (n : ), f (n x) = n f x) (npow : ∀ (x : β) (n : ), f (x ^ n) = f x ^ n) (nat_cast : ∀ (n : ), f n = n) (int_cast : ∀ (n : ), f n = n) :
ring β

Pullback a `ring` instance along an injective function. See note [reducible non-instances].

Equations
@[protected, reducible]
def function.surjective.ring {α : Type u} {β : Type v} [ring α] [has_zero β] [has_one β] [has_add β] [has_mul β] [has_neg β] [has_sub β] [ β] [ β] [ ] [has_nat_cast β] [has_int_cast β] (f : α → β) (hf : function.surjective f) (zero : f 0 = 0) (one : f 1 = 1) (add : ∀ (x y : α), f (x + y) = f x + f y) (mul : ∀ (x y : α), f (x * y) = f x * f y) (neg : ∀ (x : α), f (-x) = -f x) (sub : ∀ (x y : α), f (x - y) = f x - f y) (nsmul : ∀ (x : α) (n : ), f (n x) = n f x) (zsmul : ∀ (x : α) (n : ), f (n x) = n f x) (npow : ∀ (x : α) (n : ), f (x ^ n) = f x ^ n) (nat_cast : ∀ (n : ), f n = n) (int_cast : ∀ (n : ), f n = n) :
ring β

Pushforward a `ring` instance along a surjective function. See note [reducible non-instances].

Equations
@[protected, instance]
def units.has_neg {α : Type u} [ring α] :

Each element of the group of units of a ring has an additive inverse.

Equations
@[protected, simp, norm_cast]
theorem units.coe_neg {α : Type u} [ring α] (u : αˣ) :

Representing an element of a ring's unit group as an element of the ring commutes with mapping this element to its additive inverse.

@[protected, simp, norm_cast]
theorem units.coe_neg_one {α : Type u} [ring α] :
-1 = -1
@[protected, instance]
def units.has_distrib_neg {α : Type u} [ring α] :
Equations
theorem units.neg_divp {α : Type u} [ring α] (a : α) (u : αˣ) :
-(a /ₚ u) = -a /ₚ u
theorem units.divp_add_divp_same {α : Type u} [ring α] (a b : α) (u : αˣ) :
a /ₚ u + b /ₚ u = (a + b) /ₚ u
theorem units.divp_sub_divp_same {α : Type u} [ring α] (a b : α) (u : αˣ) :
a /ₚ u - b /ₚ u = (a - b) /ₚ u
theorem units.add_divp {α : Type u} [ring α] (a b : α) (u : αˣ) :
a + b /ₚ u = (a * u + b) /ₚ u
theorem units.sub_divp {α : Type u} [ring α] (a b : α) (u : αˣ) :
a - b /ₚ u = (a * u - b) /ₚ u
theorem units.divp_add {α : Type u} [ring α] (a b : α) (u : αˣ) :
a /ₚ u + b = (a + b * u) /ₚ u
theorem units.divp_sub {α : Type u} [ring α] (a b : α) (u : αˣ) :
a /ₚ u - b = (a - b * u) /ₚ u
theorem is_unit.neg {α : Type u} [ring α] {a : α} :
is_unit (-a)
theorem is_unit.neg_iff {α : Type u} [ring α] (a : α) :
theorem is_unit.sub_iff {α : Type u} [ring α] {x y : α} :
is_unit (x - y) is_unit (y - x)
@[class]
structure non_unital_comm_ring (α : Type u) :
Type u
• add : α → α → α
• add_assoc : ∀ (a b c : α), a + b + c = a + (b + c)
• zero : α
• zero_add : ∀ (a : α), 0 + a = a
• add_zero : ∀ (a : α), a + 0 = a
• nsmul : α → α
• nsmul_zero' : (∀ (x : α), . "try_refl_tac"
• nsmul_succ' : (∀ (n : ) (x : α), . "try_refl_tac"
• neg : α → α
• sub : α → α → α
• sub_eq_add_neg : (∀ (a b : α), a - b = a + -b) . "try_refl_tac"
• zsmul : α → α
• zsmul_zero' : (∀ (a : α), . "try_refl_tac"
• zsmul_succ' : (∀ (n : ) (a : α), . "try_refl_tac"
• zsmul_neg' : (∀ (n : ) (a : α), . "try_refl_tac"
• add_left_neg : ∀ (a : α), -a + a = 0
• add_comm : ∀ (a b : α), a + b = b + a
• mul : α → α → α
• left_distrib : ∀ (a b c : α), a * (b + c) = a * b + a * c
• right_distrib : ∀ (a b c : α), (a + b) * c = a * c + b * c
• zero_mul : ∀ (a : α), 0 * a = 0
• mul_zero : ∀ (a : α), a * 0 = 0
• mul_assoc : ∀ (a b c : α), a * b * c = a * (b * c)
• mul_comm : ∀ (a b : α), a * b = b * a

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]
@[instance]
@[protected, instance]
Equations
@[instance]
def comm_ring.to_ring (α : Type u) [self : comm_ring α] :
ring α
Instances for `comm_ring.to_ring`
@[class]
structure comm_ring (α : Type u) :
Type u
• add : α → α → α
• add_assoc : ∀ (a b c : α), a + b + c = a + (b + c)
• zero : α
• zero_add : ∀ (a : α), 0 + a = a
• add_zero : ∀ (a : α), a + 0 = a
• nsmul : α → α
• nsmul_zero' : (∀ (x : α), = 0) . "try_refl_tac"
• nsmul_succ' : (∀ (n : ) (x : α), = x + x) . "try_refl_tac"
• neg : α → α
• sub : α → α → α
• sub_eq_add_neg : (∀ (a b : α), a - b = a + -b) . "try_refl_tac"
• zsmul : α → α
• zsmul_zero' : (∀ (a : α), = 0) . "try_refl_tac"
• zsmul_succ' : (∀ (n : ) (a : α), = a + a) . "try_refl_tac"
• zsmul_neg' : (∀ (n : ) (a : α), = - a) . "try_refl_tac"
• add_left_neg : ∀ (a : α), -a + a = 0
• add_comm : ∀ (a b : α), a + b = b + a
• int_cast : → α
• nat_cast : → α
• one : α
• nat_cast_zero : . "control_laws_tac"
• nat_cast_succ : (∀ (n : ), comm_ring.nat_cast (n + 1) = . "control_laws_tac"
• int_cast_of_nat : (∀ (n : ), . "control_laws_tac"
• int_cast_neg_succ_of_nat : (∀ (n : ), comm_ring.int_cast (-(n + 1)) = -(n + 1)) . "control_laws_tac"
• mul : α → α → α
• mul_assoc : ∀ (a b c : α), a * b * c = a * (b * c)
• one_mul : ∀ (a : α), 1 * a = a
• mul_one : ∀ (a : α), a * 1 = a
• npow : α → α
• npow_zero' : (∀ (x : α), = 1) . "try_refl_tac"
• npow_succ' : (∀ (n : ) (x : α), = x * x) . "try_refl_tac"
• left_distrib : ∀ (a b c : α), a * (b + c) = a * b + a * c
• right_distrib : ∀ (a b c : α), (a + b) * c = a * c + b * c
• mul_comm : ∀ (a b : α), a * b = b * a

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 α] :
@[protected, instance]
def comm_ring.to_comm_semiring {α : Type u} [s : comm_ring α] :
Equations
@[protected, instance]
def comm_ring.to_non_unital_comm_ring {α : Type u} [s : comm_ring α] :
Equations
theorem dvd_sub {α : Type u} {a b c : α} (h₁ : a b) (h₂ : a c) :
a b - c
theorem dvd_add_iff_left {α : Type u} {a b c : α} (h : a c) :
a b a b + c
theorem dvd_add_iff_right {α : Type u} {a b c : α} (h : a b) :
a c a b + c
theorem dvd_add_left {α : Type u} {a b c : α} (h : a c) :
a b + c a b

If an element a divides another element c in a commutative ring, a divides the sum of another element b with c iff a divides b.

theorem dvd_add_right {α : Type u} {a b c : α} (h : a b) :
a b + c a c

If an element a divides another element b in a commutative ring, a divides the sum of b and another element c iff a divides c.

theorem dvd_iff_dvd_of_dvd_sub {α : Type u} {a b c : α} (h : a b - c) :
a b a c
theorem two_dvd_bit1 {α : Type u} [ring α] {a : α} :
2 bit1 a 2 1
@[simp]
theorem dvd_add_self_left {α : Type u} [ring α] {a b : α} :
a a + b a b

An element a divides the sum a + b if and only if a divides b.

@[simp]
theorem dvd_add_self_right {α : Type u} [ring α] {a b : α} :
a b + a a b

An element a divides the sum b + a if and only if a divides b.

@[protected, reducible]
def function.injective.non_unital_comm_ring {α : Type u} {β : Type v} [has_zero β] [has_add β] [has_mul β] [has_neg β] [has_sub β] [ β] [ β] (f : β → α) (hf : function.injective f) (zero : f 0 = 0) (add : ∀ (x y : β), f (x + y) = f x + f y) (mul : ∀ (x y : β), f (x * y) = f x * f y) (neg : ∀ (x : β), f (-x) = -f x) (sub : ∀ (x y : β), f (x - y) = f x - f y) (nsmul : ∀ (x : β) (n : ), f (n x) = n f x) (zsmul : ∀ (x : β) (n : ), f (n x) = n f x) :

Pullback a `comm_ring` instance along an injective function. See note [reducible non-instances].

Equations
@[protected, reducible]
def function.surjective.non_unital_comm_ring {α : Type u} {β : Type v} [has_zero β] [has_add β] [has_mul β] [has_neg β] [has_sub β] [ β] [ β] (f : α → β) (hf : function.surjective f) (zero : f 0 = 0) (add : ∀ (x y : α), f (x + y) = f x + f y) (mul : ∀ (x y : α), f (x * y) = f x * f y) (neg : ∀ (x : α), f (-x) = -f x) (sub : ∀ (x y : α), f (x - y) = f x - f y) (nsmul : ∀ (x : α) (n : ), f (n x) = n f x) (zsmul : ∀ (x : α) (n : ), f (n x) = n f x) :

Pushforward a `non_unital_comm_ring` instance along a surjective function. See note [reducible non-instances].

Equations
theorem Vieta_formula_quadratic {α : Type u} {b c x : α} (h : x * x - b * x + c = 0) :
∃ (y : α), y * y - b * y + c = 0 x + y = b x * y = c

Vieta's formula for a quadratic equation, relating the coefficients of the polynomial with its roots. This particular version states that if we have a root `x` of a monic quadratic polynomial, then there is another root `y` such that `x + y` is negative the `a_1` coefficient and `x * y` is the `a_0` coefficient.

theorem dvd_mul_sub_mul {α : Type u} {k a b x y : α} (hab : k a - b) (hxy : k x - y) :
k a * x - b * y
@[protected, reducible]
def function.injective.comm_ring {α : Type u} {β : Type v} [comm_ring α] [has_zero β] [has_one β] [has_add β] [has_mul β] [has_neg β] [has_sub β] [ β] [ β] [ ] [has_nat_cast β] [has_int_cast β] (f : β → α) (hf : function.injective f) (zero : f 0 = 0) (one : f 1 = 1) (add : ∀ (x y : β), f (x + y) = f x + f y) (mul : ∀ (x y : β), f (x * y) = f x * f y) (neg : ∀ (x : β), f (-x) = -f x) (sub : ∀ (x y : β), f (x - y) = f x - f y) (nsmul : ∀ (x : β) (n : ), f (n x) = n f x) (zsmul : ∀ (x : β) (n : ), f (n x) = n f x) (npow : ∀ (x : β) (n : ), f (x ^ n) = f x ^ n) (nat_cast : ∀ (n : ), f n = n) (int_cast : ∀ (n : ), f n = n) :

Pullback a `comm_ring` instance along an injective function. See note [reducible non-instances].

Equations
@[protected, reducible]
def function.surjective.comm_ring {α : Type u} {β : Type v} [comm_ring α] [has_zero β] [has_one β] [has_add β] [has_mul β] [has_neg β] [has_sub β] [ β] [ β] [ ] [has_nat_cast β] [has_int_cast β] (f : α → β) (hf : function.surjective f) (zero : f 0 = 0) (one : f 1 = 1) (add : ∀ (x y : α), f (x + y) = f x + f y) (mul : ∀ (x y : α), f (x * y) = f x * f y) (neg : ∀ (x : α), f (-x) = -f x) (sub : ∀ (x y : α), f (x - y) = f x - f y) (nsmul : ∀ (x : α) (n : ), f (n x) = n f x) (zsmul : ∀ (x : α) (n : ), f (n x) = n f x) (npow : ∀ (x : α) (n : ), f (x ^ n) = f x ^ n) (nat_cast : ∀ (n : ), f n = n) (int_cast : ∀ (n : ), f n = n) :

Pushforward a `comm_ring` instance along a surjective function. See note [reducible non-instances].

Equations
theorem succ_ne_self {α : Type u} [nontrivial α] (a : α) :
a + 1 a
theorem pred_ne_self {α : Type u} [nontrivial α] (a : α) :
a - 1 a
theorem is_left_regular_of_non_zero_divisor {α : Type u} (k : α) (h : ∀ (x : α), k * x = 0x = 0) :

Left `mul` by a `k : α` over `[ring α]` is injective, if `k` is not a zero divisor. The typeclass that restricts all terms of `α` to have this property is `no_zero_divisors`.

theorem is_right_regular_of_non_zero_divisor {α : Type u} (k : α) (h : ∀ (x : α), x * k = 0x = 0) :

Right `mul` by a `k : α` over `[ring α]` is injective, if `k` is not a zero divisor. The typeclass that restricts all terms of `α` to have this property is `no_zero_divisors`.

theorem is_regular_of_ne_zero' {α : Type u} {k : α} (hk : k 0) :
theorem is_regular_iff_ne_zero' {α : Type u} [nontrivial α] {k : α} :
k 0
@[reducible]

A ring with no zero divisors is a `cancel_monoid_with_zero`.

Note this is not an instance as it forms a typeclass loop.

Equations
@[reducible]

A commutative ring with no zero divisors is a `cancel_comm_monoid_with_zero`.

Note this is not an instance as it forms a typeclass loop.

Equations
@[instance]
def is_domain.to_no_zero_divisors (α : Type u) [ring α] [self : is_domain α] :
@[class]
structure is_domain (α : Type u) [ring α] :
Prop
• eq_zero_or_eq_zero_of_mul_eq_zero : ∀ {a b : α}, a * b = 0a = 0 b = 0
• exists_pair_ne : ∃ (x y : α), x y

A domain is a nontrivial ring with no zero divisors, i.e. satisfying the condition `a * b = 0 ↔ a = 0 ∨ b = 0`.

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

Instances of this typeclass
@[instance]
def is_domain.to_nontrivial (α : Type u) [ring α] [self : is_domain α] :
@[protected, instance]
def is_domain.to_cancel_monoid_with_zero {α : Type u} [ring α] [is_domain α] :
Equations
@[protected, instance]
Equations
@[simp]
theorem semiconj_by.add_right {R : Type x} [distrib R] {a x y x' y' : R} (h : x y) (h' : x' y') :
(x + x') (y + y')
@[simp]
theorem semiconj_by.add_left {R : Type x} [distrib R] {a b x y : R} (ha : x y) (hb : x y) :
semiconj_by (a + b) x y
theorem semiconj_by.neg_right {R : Type x} [has_mul R] {a x y : R} (h : x y) :
(-x) (-y)
@[simp]
theorem semiconj_by.neg_right_iff {R : Type x} [has_mul R] {a x y : R} :
(-x) (-y) x y
theorem semiconj_by.neg_left {R : Type x} [has_mul R] {a x y : R} (h : x y) :
semiconj_by (-a) x y
@[simp]
theorem semiconj_by.neg_left_iff {R : Type x} [has_mul R] {a x y : R} :
semiconj_by (-a) x y x y
@[simp]
theorem semiconj_by.neg_one_right {R : Type x} (a : R) :
(-1) (-1)
@[simp]
theorem semiconj_by.neg_one_left {R : Type x} (x : R) :
semiconj_by (-1) x x
@[simp]
theorem semiconj_by.sub_right {R : Type x} {a x y x' y' : R} (h : x y) (h' : x' y') :
(x - x') (y - y')
@[simp]
theorem semiconj_by.sub_left {R : Type x} {a b x y : R} (ha : x y) (hb : x y) :
semiconj_by (a - b) x y
@[simp]
theorem commute.add_right {R : Type x} [distrib R] {a b c : R} :
b c (b + c)
@[simp]
theorem commute.add_left {R : Type x} [distrib R] {a b c : R} :
c ccommute (a + b) c
theorem commute.bit0_right {R : Type x} [distrib R] {x y : R} (h : y) :
(bit0 y)
theorem commute.bit0_left {R : Type x} [distrib R] {x y : R} (h : y) :
theorem commute.bit1_right {R : Type x} {x y : R} (h : y) :
(bit1 y)
theorem commute.bit1_left {R : Type x} {x y : R} (h : y) :
theorem commute.mul_self_sub_mul_self_eq {R : Type x} {a b : R} (h : 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 x} {a b : R} (h : b) :
a * a - b * b = (a - b) * (a + b)
theorem commute.mul_self_eq_mul_self_iff {R : Type x} {a b : R} (h : b) :
a * a = b * b a = b a = -b
theorem commute.neg_right {R : Type x} [has_mul R] {a b : R} :
b (-b)
@[simp]
theorem commute.neg_right_iff {R : Type x} [has_mul R] {a b : R} :
(-b) b
theorem commute.neg_left {R : Type x} [has_mul R] {a b : R} :
bcommute (-a) b
@[simp]
theorem commute.neg_left_iff {R : Type x} [has_mul R] {a b : R} :
commute (-a) b