mathlib documentation

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 #

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]
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
@[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

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) :
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 : α), non_unital_semiring.nsmul 0 x = 0) . "try_refl_tac"
  • nsmul_succ' : (∀ (n : ) (x : α), non_unital_semiring.nsmul n.succ x = x + non_unital_semiring.nsmul 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
@[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
@[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 : α), semiring.nsmul 0 x = 0) . "try_refl_tac"
  • nsmul_succ' : (∀ (n : ) (x : α), semiring.nsmul n.succ x = x + semiring.nsmul 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)
  • one : α
  • one_mul : ∀ (a : α), 1 * a = a
  • mul_one : ∀ (a : α), a * 1 = a
  • nat_cast : → α
  • nat_cast_zero : semiring.nat_cast 0 = 0 . "control_laws_tac"
  • nat_cast_succ : (∀ (n : ), semiring.nat_cast (n + 1) = semiring.nat_cast n + 1) . "control_laws_tac"
  • npow : α → α
  • npow_zero' : (∀ (x : α), semiring.npow 0 x = 1) . "try_refl_tac"
  • npow_succ' : (∀ (n : ) (x : α), semiring.npow n.succ x = x * semiring.npow n 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 β] [has_smul β] {α : Type u} [non_unital_non_assoc_semiring α] (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 β] [has_smul β] {α : Type u} [non_unital_semiring α] (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} [non_assoc_semiring α] {β : Type v} [has_zero β] [has_one β] [has_mul β] [has_add β] [has_smul β] [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_pow β ] [has_smul β] [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 β] [has_smul β] {α : Type u} [non_unital_non_assoc_semiring α] (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 β] [has_smul β] {α : Type u} [non_unital_semiring α] (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} [non_assoc_semiring α] {β : Type v} [has_zero β] [has_one β] [has_add β] [has_mul β] [has_smul β] [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_pow β ] [has_smul β] [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 one_add_one_eq_two {α : Type u} [has_one α] [has_add α] :
1 + 1 = 2
theorem dvd_add {α : Type u} [has_add α] [semigroup α] [left_distrib_class α] {a b c : α} (h₁ : a b) (h₂ : a c) :
a b + c
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
def add_hom.mul_left {R : Type u_1} [distrib 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) :
(add_hom.mul_right r) = λ (a : R), a * r
def add_hom.mul_right {R : Type u_1} [distrib 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} [non_assoc_semiring α] [non_assoc_semiring β] [add_hom_class F α β] (f : F) (a : α) :
f (bit0 a) = bit0 (f a)

Additive homomorphisms preserve bit0.

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

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

Equations
def add_monoid_hom.mul_right {R : Type u_1} [non_unital_non_assoc_semiring R] (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} [non_unital_non_assoc_semiring R] (r : R) :
(add_monoid_hom.mul_right r) = λ (_x : R), _x * 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 : α), non_unital_comm_semiring.nsmul 0 x = 0) . "try_refl_tac"
  • nsmul_succ' : (∀ (n : ) (x : α), non_unital_comm_semiring.nsmul n.succ x = x + non_unital_comm_semiring.nsmul 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
@[protected, reducible]
def function.injective.non_unital_comm_semiring {α : Type u} {γ : Type w} [non_unital_comm_semiring α] [has_zero γ] [has_add γ] [has_mul γ] [has_smul γ] (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} [non_unital_comm_semiring α] [has_zero γ] [has_add γ] [has_mul γ] [has_smul γ] (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} [non_unital_comm_semiring α] {d x y : α} (hdx : d x) (hdy : d y) (a b : α) :
d a * x + b * y
@[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
@[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, reducible]
def function.injective.comm_semiring {α : Type u} {γ : Type w} [comm_semiring α] [has_zero γ] [has_one γ] [has_add γ] [has_mul γ] [has_smul γ] [has_nat_cast γ] [has_pow γ ] (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} [comm_semiring α] [has_zero γ] [has_one γ] [has_add γ] [has_mul γ] [has_smul γ] [has_nat_cast γ] [has_pow γ ] (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} [comm_semiring α] (a b : α) :
(a + b) * (a + b) = a * a + 2 * a * b + b * b
@[instance]
@[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
@[protected, reducible]
def function.injective.has_distrib_neg {α : Type u} {β : Type v} [has_mul α] [has_distrib_neg α] [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_distrib_neg α] [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
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.

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

Prefer neg_zero if subtraction_monoid is available.

theorem dvd_neg_of_dvd {α : Type u} [semigroup α] [has_distrib_neg α] {a b : α} (h : a b) :
a -b
theorem dvd_of_dvd_neg {α : Type u} [semigroup α] [has_distrib_neg α] {a b : α} (h : a -b) :
a b
@[simp]
theorem dvd_neg {α : Type u} [semigroup α] [has_distrib_neg α] (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 α] [has_distrib_neg α] {a b : α} (h : a b) :
-a b
theorem dvd_of_neg_dvd {α : Type u} [semigroup α] [has_distrib_neg α] {a b : α} (h : -a b) :
a b
@[simp]
theorem neg_dvd {α : Type u} [semigroup α] [has_distrib_neg α] (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 α] [has_distrib_neg α] (a : α) :

Rings #

@[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
@[protected, reducible]
def function.injective.non_unital_non_assoc_ring {α : Type u} {β : Type v} [non_unital_non_assoc_ring α] [has_zero β] [has_add β] [has_mul β] [has_neg β] [has_sub β] [has_smul β] [has_smul β] (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} [non_unital_non_assoc_ring α] [has_zero β] [has_add β] [has_mul β] [has_neg β] [has_sub β] [has_smul β] [has_smul β] (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
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.

@[instance]
@[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
@[protected, reducible]
def function.injective.non_unital_ring {α : Type u} {β : Type v} [non_unital_ring α] [has_zero β] [has_add β] [has_mul β] [has_neg β] [has_sub β] [has_smul β] [has_smul β] (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} [non_unital_ring α] [has_zero β] [has_add β] [has_mul β] [has_neg β] [has_sub β] [has_smul β] [has_smul β] (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

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]
@[instance]
@[protected, reducible]
def function.injective.non_assoc_ring {α : Type u} {β : Type v} [non_assoc_ring α] [has_zero β] [has_one β] [has_add β] [has_mul β] [has_neg β] [has_sub β] [has_smul β] [has_smul β] [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} [non_assoc_ring α] [has_zero β] [has_one β] [has_add β] [has_mul β] [has_neg β] [has_sub β] [has_smul β] [has_smul β] [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} [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
@[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 : α), ring.nsmul 0 x = 0) . "try_refl_tac"
  • nsmul_succ' : (∀ (n : ) (x : α), ring.nsmul n.succ x = x + ring.nsmul n x) . "try_refl_tac"
  • neg : α → α
  • sub : α → α → α
  • sub_eq_add_neg : (∀ (a b : α), a - b = a + -b) . "try_refl_tac"
  • zsmul : α → α
  • zsmul_zero' : (∀ (a : α), ring.zsmul 0 a = 0) . "try_refl_tac"
  • zsmul_succ' : (∀ (n : ) (a : α), ring.zsmul (int.of_nat n.succ) a = a + ring.zsmul (int.of_nat n) a) . "try_refl_tac"
  • zsmul_neg' : (∀ (n : ) (a : α), ring.zsmul -[1+ n] 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 : ring.nat_cast 0 = 0 . "control_laws_tac"
  • nat_cast_succ : (∀ (n : ), ring.nat_cast (n + 1) = ring.nat_cast n + 1) . "control_laws_tac"
  • int_cast_of_nat : (∀ (n : ), ring.int_cast 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 : α), ring.npow 0 x = 1) . "try_refl_tac"
  • npow_succ' : (∀ (n : ) (x : α), ring.npow n.succ x = x * ring.npow n 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_smul β] [has_smul β] [has_pow β ] [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_smul β] [has_smul β] [has_pow β ] [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 ais_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

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]
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

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 α] :
theorem dvd_sub {α : Type u} [non_unital_ring α] {a b c : α} (h₁ : a b) (h₂ : a c) :
a b - c
theorem dvd_add_iff_left {α : Type u} [non_unital_ring α] {a b c : α} (h : a c) :
a b a b + c
theorem dvd_add_iff_right {α : Type u} [non_unital_ring α] {a b c : α} (h : a b) :
a c a b + c
theorem dvd_add_left {α : Type u} [non_unital_ring α] {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} [non_unital_ring α] {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} [non_unital_ring α] {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} [non_unital_comm_ring α] [has_zero β] [has_add β] [has_mul β] [has_neg β] [has_sub β] [has_smul β] [has_smul β] (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} [non_unital_comm_ring α] [has_zero β] [has_add β] [has_mul β] [has_neg β] [has_sub β] [has_smul β] [has_smul β] (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} [non_unital_comm_ring α] {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} [non_unital_comm_ring α] {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_smul β] [has_smul β] [has_pow β ] [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_smul β] [has_smul β] [has_pow β ] [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} [non_assoc_ring α] [nontrivial α] (a : α) :
a + 1 a
theorem pred_ne_self {α : Type u} [non_assoc_ring α] [nontrivial α] (a : α) :
a - 1 a
theorem is_left_regular_of_non_zero_divisor {α : Type u} [non_unital_non_assoc_ring α] (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} [non_unital_non_assoc_ring α] (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} [non_unital_non_assoc_ring α] [no_zero_divisors α] {k : α} (hk : k 0) :
theorem is_regular_iff_ne_zero' {α : Type u} [nontrivial α] [non_unital_non_assoc_ring α] [no_zero_divisors α] {k : α} :
@[instance]
def is_domain.to_no_zero_divisors (α : Type u) [ring α] [self : is_domain α] :
@[instance]
def is_domain.to_nontrivial (α : Type u) [ring α] [self : is_domain α] :
@[simp]
theorem semiconj_by.add_right {R : Type x} [distrib R] {a x y x' y' : R} (h : semiconj_by a x y) (h' : semiconj_by a x' y') :
semiconj_by a (x + x') (y + y')
@[simp]
theorem semiconj_by.add_left {R : Type x} [distrib R] {a b x y : R} (ha : semiconj_by a x y) (hb : semiconj_by b x y) :
semiconj_by (a + b) x y
theorem semiconj_by.neg_right {R : Type x} [has_mul R] [has_distrib_neg R] {a x y : R} (h : semiconj_by a x y) :
semiconj_by a (-x) (-y)
@[simp]
theorem semiconj_by.neg_right_iff {R : Type x} [has_mul R] [has_distrib_neg R] {a x y : R} :
semiconj_by a (-x) (-y) semiconj_by a x y
theorem semiconj_by.neg_left {R : Type x} [has_mul R] [has_distrib_neg R] {a x y : R} (h : semiconj_by a x y) :
semiconj_by (-a) x y
@[simp]
theorem semiconj_by.neg_left_iff {R : Type x} [has_mul R] [has_distrib_neg R] {a x y : R} :
@[simp]
theorem semiconj_by.neg_one_right {R : Type x} [mul_one_class R] [has_distrib_neg R] (a : R) :
semiconj_by a (-1) (-1)
@[simp]
theorem semiconj_by.neg_one_left {R : Type x} [mul_one_class R] [has_distrib_neg R] (x : R) :
semiconj_by (-1) x x
@[simp]
theorem semiconj_by.sub_right {R : Type x} [non_unital_non_assoc_ring R] {a x y x' y' : R} (h : semiconj_by a x y) (h' : semiconj_by a x' y') :
semiconj_by a (x - x') (y - y')
@[simp]
theorem semiconj_by.sub_left {R : Type x} [non_unital_non_assoc_ring R] {a b x y : R} (ha : semiconj_by a x y) (hb : semiconj_by b x y) :
semiconj_by (a - b) x y
@[simp]
theorem commute.add_right {R : Type x} [distrib R] {a b c : R} :
commute a bcommute a ccommute a (b + c)
@[simp]
theorem commute.add_left {R : Type x} [distrib R] {a b c : R} :
commute a ccommute b ccommute (a + b) c
theorem commute.bit0_right {R : Type x} [distrib R] {x y : R} (h : commute x y) :
theorem commute.bit0_left {R : Type x} [distrib R] {x y : R} (h : commute x y) :
theorem commute.bit1_right {R : Type x} [non_assoc_semiring R] {x y : R} (h : commute x y) :
theorem commute.bit1_left {R : Type x} [non_assoc_semiring R] {x y : R} (h : commute x y) :
theorem commute.mul_self_sub_mul_self_eq {R : Type x} [non_unital_non_assoc_ring R] {a b : R} (h : commute a b) :
a * a - b * b = (a + b) * (a - b)

Representation of a difference of two squares of commuting elements as a product.

theorem commute.mul_self_sub_mul_self_eq' {R : Type x} [non_unital_non_assoc_ring R] {a b : R} (h : commute a b) :
a * a - b * b = (a - b) * (a + b)
theorem commute.mul_self_eq_mul_self_iff {R : Type x} [non_unital_non_assoc_ring R] [no_zero_divisors R] {a b : R} (h : commute a b) :
a * a = b * b a = b a = -b
theorem commute.neg_right {R : Type x} [has_mul R] [has_distrib_neg R] {a b : R} :
commute a bcommute a (-b)
@[simp]
theorem commute.neg_right_iff {R : Type x} [has_mul R] [has_distrib_neg R] {a b : R} :
commute a (-b) commute a b
theorem commute.neg_left {R : Type x} [has_mul R] [has_distrib_neg R] {a b : R} :
commute a bcommute (-a) b
@[simp]
theorem commute.neg_left_iff {R : Type x} [has_mul R] [has_distrib_neg R] {a b : R} :
commute (-a) b commute a b
@[simp]
theorem commute.neg_one_right {R : Type x} [mul_one_class R] [has_distrib_neg R] (a : R) :
commute a (-1)
@[simp]
theorem commute.neg_one_left {R : Type x} [mul_one_class R] [has_distrib_neg R] (a : R) :
commute (-1) a
@[simp]
theorem commute.sub_right {R : Type x} [non_unital_non_assoc_ring R] {a b c : R} :
commute a bcommute a ccommute a (b - c)
@[simp]
theorem commute.sub_left {R : Type x} [non_unital_non_assoc_ring R] {a b c : R} :
commute a ccommute b ccommute (a - b) c
theorem mul_self_sub_mul_self {R : Type x} [comm_ring R] (a b : R) :
a * a - b * b = (a + b) * (a - b)

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

theorem mul_self_sub_one {R : Type x} [non_assoc_ring R] (a : R) :
a * a - 1 = (a + 1) * (a - 1)
theorem mul_self_eq_mul_self_iff {R : Type x} [comm_ring R] [no_zero_divisors R] {a b : R} :
a * a = b * b a = b a = -b
theorem mul_self_eq_one_iff {R : Type x} [non_assoc_ring R] [no_zero_divisors R] {a : R} :
a * a = 1 a = 1 a = -1
theorem units.divp_add_divp {α : Type u} [comm_ring α] (a b : α) (u₁ u₂ : αˣ) :
a /ₚ u₁ + b /ₚ u₂ = (a * u₂ + u₁ * b) /ₚ (u₁ * u₂)
theorem units.divp_sub_divp {α : Type u} [comm_ring α] (a b : α) (u₁ u₂ : αˣ) :
a /ₚ u₁ - b /ₚ u₂ = (a * u₂ - u₁ * b) /ₚ (u₁ * u₂)
theorem units.inv_eq_self_iff {R : Type x} [ring R] [no_zero_divisors R] (u : Rˣ) :
u⁻¹ = u u = 1 u = -1

In the unit group of an integral domain, a unit is its own inverse iff the unit is one or one's additive inverse.

Order dual #

@[protected, instance]
def order_dual.distrib {α : Type u} [h : distrib α] :
Equations
@[protected, instance]
Equations
@[protected, instance]
Equations
@[protected, instance]
Equations
@[protected, instance]
Equations
@[protected, instance]
def order_dual.semiring {α : Type u} [h : semiring α] :
Equations
@[protected, instance]
Equations
@[protected, instance]
Equations
@[protected, instance]
Equations
@[protected, instance]
Equations
@[protected, instance]
def order_dual.ring {α : Type u} [h : ring α] :
Equations
@[protected, instance]
def order_dual.comm_ring {α : Type u} [h : comm_ring α] :
Equations
@[protected, instance]
def order_dual.is_domain {α : Type u} [ring α] [h : is_domain α] :

Lexicographical order #

@[protected, instance]
def lex.distrib {α : Type u} [h : distrib α] :
Equations
@[protected, instance]
def lex.left_distrib_class {α : Type u} [has_mul α] [has_add α] [h : left_distrib_class α] :
Equations
@[protected, instance]
def lex.right_distrib_class {α : Type u} [has_mul α] [has_add α] [h : right_distrib_class α] :
Equations
@[protected, instance]
Equations
@[protected, instance]
Equations
@[protected, instance]
def lex.semiring {α : Type u} [h : semiring α] :
Equations
@[protected, instance]
Equations
@[protected, instance]
def lex.comm_semiring {α : Type u} [h : comm_semiring α] :
Equations
@[protected, instance]
def lex.has_distrib_neg {α : Type u} [has_mul α] [h : has_distrib_neg α] :
Equations
@[protected, instance]
def lex.non_unital_ring {α : Type u} [h : non_unital_ring α] :
Equations
@[protected, instance]
def lex.non_assoc_ring {α : Type u} [h : non_assoc_ring α] :
Equations
@[protected, instance]
def lex.ring {α : Type u} [h : ring α] :
ring (lex α)
Equations
@[protected, instance]
Equations
@[protected, instance]
def lex.comm_ring {α : Type u} [h : comm_ring α] :
Equations
@[protected, instance]
def lex.is_domain {α : Type u} [ring α] [h : is_domain α] :