mathlib documentation

algebra.ring.basic

Properties and homomorphisms of semirings and rings #

This file proves simple properties of semirings, rings and domains and their unit groups. It also defines bundled homomorphisms of semirings and rings. As with monoid and groups, we use the same structure ring_hom a β, a.k.a. α →+* β, for both homomorphism types.

The unbundled homomorphisms are defined in deprecated/ring. They are deprecated and the plan is to slowly remove them from mathlib.

Main definitions #

ring_hom, nonzero, domain, is_domain

Notations #

→+* for bundled ring homs (also use for semiring homs)

Implementation notes #

Tags #

ring_hom, semiring_hom, 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
@[instance]
def distrib.to_has_add (R : Type u_1) [self : distrib R] :
theorem left_distrib {R : Type x} [distrib R] (a b c : R) :
a * (b + c) = a * b + a * c
theorem mul_add {R : Type x} [distrib R] (a b c : R) :
a * (b + c) = a * b + a * c

Alias of left_distrib.

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

Alias of right_distrib.

@[protected]
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]
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
@[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
@[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 : α), non_assoc_semiring.nsmul 0 x = 0) . "try_refl_tac"
  • nsmul_succ' : (∀ (n : ) (x : α), non_assoc_semiring.nsmul n.succ x = x + non_assoc_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
  • one : α
  • one_mul : ∀ (a : α), 1 * a = a
  • mul_one : ∀ (a : α), a * 1 = a

A unital but not-necessarily-associative semiring.

Instances
@[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
  • 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
@[instance]
def semiring.to_non_unital_semiring (α : Type u) [self : semiring α] :
@[instance]
def semiring.to_monoid_with_zero (α : Type u) [self : semiring α] :
@[protected]
def function.injective.non_unital_non_assoc_semiring {β : Type v} [has_zero β] [has_add β] [has_mul β] {α : 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) :

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

Equations
@[protected]
def function.injective.non_unital_semiring {β : Type v} [has_zero β] [has_add β] [has_mul β] {α : 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) :

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

Equations
@[protected]
def function.injective.non_assoc_semiring {β : Type v} [has_zero β] [has_add β] [has_mul β] {α : Type u} [non_assoc_semiring α] [has_one β] (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) :

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

Equations
@[protected]
def function.injective.semiring {β : Type v} [has_zero β] [has_add β] [has_mul β] {α : Type u} [semiring α] [has_one β] (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) :

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

Equations
@[protected]
def function.surjective.non_unital_non_assoc_semiring {β : Type v} [has_zero β] [has_add β] [has_mul β] {α : 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) :

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

Equations
@[protected]
def function.surjective.non_unital_semiring {β : Type v} [has_zero β] [has_add β] [has_mul β] {α : 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) :

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

Equations
@[protected]
def function.surjective.non_assoc_semiring {β : Type v} [has_zero β] [has_add β] [has_mul β] {α : Type u} [non_assoc_semiring α] [has_one β] (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) :

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

Equations
@[protected]
def function.surjective.semiring {β : Type v} [has_zero β] [has_add β] [has_mul β] {α : Type u} [semiring α] [has_one β] (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) :

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

Equations
theorem one_add_one_eq_two {α : Type u} [semiring α] :
1 + 1 = 2
theorem two_mul {α : Type u} [semiring α] (n : α) :
2 * n = n + n
theorem distrib_three_right {α : Type u} [semiring α] (a b c d : α) :
(a + b + c) * d = a * d + b * d + c * d
theorem mul_two {α : Type u} [semiring α] (n : α) :
n * 2 = n + n
theorem bit0_eq_two_mul {α : Type u} [semiring α] (n : α) :
bit0 n = 2 * 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} [non_assoc_semiring α] (P : Prop) [decidable P] (a : α) :
a * ite P 1 0 = ite P a 0
@[simp]
theorem boole_mul {α : Type u_1} [non_assoc_semiring α] (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
def even {α : Type u} [semiring α] (a : α) :
Prop

An element a of a semiring is even if there exists k such a = 2*k.

Equations
theorem even_iff_two_dvd {α : Type u} [semiring α] {a : α} :
even a 2 a
@[simp]
theorem range_two_mul (α : Type u_1) [semiring α] :
set.range (λ (x : α), 2 * x) = {a : α | even a}
@[simp]
theorem even_bit0 {α : Type u} [semiring α] (a : α) :
def odd {α : Type u} [semiring α] (a : α) :
Prop

An element a of a semiring is odd if there exists k such a = 2*k + 1.

Equations
  • odd a = ∃ (k : α), a = 2 * k + 1
@[simp]
theorem odd_bit1 {α : Type u} [semiring α] (a : α) :
odd (bit1 a)
@[simp]
theorem range_two_mul_add_one (α : Type u_1) [semiring α] :
set.range (λ (x : α), 2 * x + 1) = {a : α | odd a}
theorem dvd_add {α : Type u} [semiring α] {a b c : α} (h₁ : a b) (h₂ : a c) :
a b + c
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
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
def ring_hom.to_add_monoid_hom {α : Type u_1} {β : Type u_2} [non_assoc_semiring α] [non_assoc_semiring β] (self : α →+* β) :
α →+ β

Reinterpret a ring homomorphism f : R →+* S as an additive monoid homomorphism R →+ S. The simp-normal form is (f : R →+ S).

def ring_hom.to_monoid_hom {α : Type u_1} {β : Type u_2} [non_assoc_semiring α] [non_assoc_semiring β] (self : α →+* β) :
α →* β

Reinterpret a ring homomorphism f : R →+* S as a monoid homomorphism R →* S. The simp-normal form is (f : R →* S).

structure ring_hom (α : Type u_1) (β : Type u_2) [non_assoc_semiring α] [non_assoc_semiring β] :
Type (max u_1 u_2)

Bundled semiring homomorphisms; use this for bundled ring homomorphisms too.

This extends from both monoid_hom and monoid_with_zero_hom in order to put the fields in a sensible order, even though monoid_with_zero_hom already extends monoid_hom.

def ring_hom.to_monoid_with_zero_hom {α : Type u_1} {β : Type u_2} [non_assoc_semiring α] [non_assoc_semiring β] (self : α →+* β) :

Reinterpret a ring homomorphism f : R →+* S as a monoid_with_zero_hom R S. The simp-normal form is (f : monoid_with_zero_hom R S).

@[instance]
def ring_hom_class.to_monoid_with_zero_hom_class (F : Type u_1) (R : out_param (Type u_2)) (S : out_param (Type u_3)) [non_assoc_semiring R] [non_assoc_semiring S] [self : ring_hom_class F R S] :
@[instance]
def ring_hom_class.to_monoid_hom_class (F : Type u_1) (R : out_param (Type u_2)) (S : out_param (Type u_3)) [non_assoc_semiring R] [non_assoc_semiring S] [self : ring_hom_class F R S] :
@[class]
structure ring_hom_class (F : Type u_1) (R : out_param (Type u_2)) (S : out_param (Type u_3)) [non_assoc_semiring R] [non_assoc_semiring S] :
Type (max u_1 u_2 u_3)

ring_hom_class F R S states that F is a type of (semi)ring homomorphisms. You should extend this class when you extend ring_hom.

This extends from both monoid_hom_class and monoid_with_zero_hom_class in order to put the fields in a sensible order, even though monoid_with_zero_hom_class already extends monoid_hom_class.

Instances
@[instance]
def ring_hom_class.to_add_monoid_hom_class (F : Type u_1) (R : out_param (Type u_2)) (S : out_param (Type u_3)) [non_assoc_semiring R] [non_assoc_semiring S] [self : ring_hom_class F R S] :
@[simp]
theorem map_bit0 {α : Type u} {β : Type v} {F : Type u_1} [non_assoc_semiring α] [non_assoc_semiring β] [ring_hom_class F α β] (f : F) (a : α) :
f (bit0 a) = bit0 (f a)

Ring homomorphisms preserve bit0.

@[simp]
theorem map_bit1 {α : Type u} {β : Type v} {F : Type u_1} [non_assoc_semiring α] [non_assoc_semiring β] [ring_hom_class F α β] (f : F) (a : α) :
f (bit1 a) = bit1 (f a)

Ring homomorphisms preserve bit1.

Throughout this section, some semiring arguments are specified with {} instead of []. See note [implicit instance arguments].

@[protected, instance]
def ring_hom.ring_hom_class {α : Type u} {β : Type v} {rα : non_assoc_semiring α} {rβ : non_assoc_semiring β} :
ring_hom_class →+* β) α β
Equations
@[protected, instance]
def ring_hom.has_coe_to_fun {α : Type u} {β : Type v} {rα : non_assoc_semiring α} {rβ : non_assoc_semiring β} :
has_coe_to_fun →+* β) (λ (_x : α →+* β), α → β)

Helper instance for when there's too many metavariables to apply to_fun.to_coe_fn directly.

Equations
@[simp]
theorem ring_hom.to_fun_eq_coe {α : Type u} {β : Type v} {rα : non_assoc_semiring α} {rβ : non_assoc_semiring β} (f : α →+* β) :
@[simp]
theorem ring_hom.coe_mk {α : Type u} {β : Type v} {rα : non_assoc_semiring α} {rβ : non_assoc_semiring β} (f : α → β) (h₁ : f 1 = 1) (h₂ : ∀ (x y : α), f (x * y) = (f x) * f y) (h₃ : f 0 = 0) (h₄ : ∀ (x y : α), f (x + y) = f x + f y) :
{to_fun := f, map_one' := h₁, map_mul' := h₂, map_zero' := h₃, map_add' := h₄} = f
@[protected, instance]
def ring_hom.has_coe_monoid_hom {α : Type u} {β : Type v} {rα : non_assoc_semiring α} {rβ : non_assoc_semiring β} :
has_coe →+* β) →* β)
Equations
@[simp, norm_cast]
theorem ring_hom.coe_monoid_hom {α : Type u} {β : Type v} {rα : non_assoc_semiring α} {rβ : non_assoc_semiring β} (f : α →+* β) :
@[simp]
theorem ring_hom.to_monoid_hom_eq_coe {α : Type u} {β : Type v} {rα : non_assoc_semiring α} {rβ : non_assoc_semiring β} (f : α →+* β) :
@[simp]
theorem ring_hom.to_monoid_with_zero_hom_eq_coe {α : Type u} {β : Type v} {rα : non_assoc_semiring α} {rβ : non_assoc_semiring β} (f : α →+* β) :
@[simp]
theorem ring_hom.coe_monoid_hom_mk {α : Type u} {β : Type v} {rα : non_assoc_semiring α} {rβ : non_assoc_semiring β} (f : α → β) (h₁ : f 1 = 1) (h₂ : ∀ (x y : α), f (x * y) = (f x) * f y) (h₃ : f 0 = 0) (h₄ : ∀ (x y : α), f (x + y) = f x + f y) :
{to_fun := f, map_one' := h₁, map_mul' := h₂, map_zero' := h₃, map_add' := h₄} = {to_fun := f, map_one' := h₁, map_mul' := h₂}
@[protected, instance]
def ring_hom.has_coe_add_monoid_hom {α : Type u} {β : Type v} {rα : non_assoc_semiring α} {rβ : non_assoc_semiring β} :
has_coe →+* β) →+ β)
Equations
@[simp, norm_cast]
theorem ring_hom.coe_add_monoid_hom {α : Type u} {β : Type v} {rα : non_assoc_semiring α} {rβ : non_assoc_semiring β} (f : α →+* β) :
@[simp]
theorem ring_hom.to_add_monoid_hom_eq_coe {α : Type u} {β : Type v} {rα : non_assoc_semiring α} {rβ : non_assoc_semiring β} (f : α →+* β) :
@[simp]
theorem ring_hom.coe_add_monoid_hom_mk {α : Type u} {β : Type v} {rα : non_assoc_semiring α} {rβ : non_assoc_semiring β} (f : α → β) (h₁ : f 1 = 1) (h₂ : ∀ (x y : α), f (x * y) = (f x) * f y) (h₃ : f 0 = 0) (h₄ : ∀ (x y : α), f (x + y) = f x + f y) :
{to_fun := f, map_one' := h₁, map_mul' := h₂, map_zero' := h₃, map_add' := h₄} = {to_fun := f, map_zero' := h₃, map_add' := h₄}
theorem ring_hom.congr_fun {α : Type u} {β : Type v} {rα : non_assoc_semiring α} {rβ : non_assoc_semiring β} {f g : α →+* β} (h : f = g) (x : α) :
f x = g x
theorem ring_hom.congr_arg {α : Type u} {β : Type v} {rα : non_assoc_semiring α} {rβ : non_assoc_semiring β} (f : α →+* β) {x y : α} (h : x = y) :
f x = f y
theorem ring_hom.coe_inj {α : Type u} {β : Type v} {rα : non_assoc_semiring α} {rβ : non_assoc_semiring β} ⦃f g : α →+* β⦄ (h : f = g) :
f = g
@[ext]
theorem ring_hom.ext {α : Type u} {β : Type v} {rα : non_assoc_semiring α} {rβ : non_assoc_semiring β} ⦃f g : α →+* β⦄ (h : ∀ (x : α), f x = g x) :
f = g
theorem ring_hom.ext_iff {α : Type u} {β : Type v} {rα : non_assoc_semiring α} {rβ : non_assoc_semiring β} {f g : α →+* β} :
f = g ∀ (x : α), f x = g x
@[simp]
theorem ring_hom.mk_coe {α : Type u} {β : Type v} {rα : non_assoc_semiring α} {rβ : non_assoc_semiring β} (f : α →+* β) (h₁ : f 1 = 1) (h₂ : ∀ (x y : α), f (x * y) = (f x) * f y) (h₃ : f 0 = 0) (h₄ : ∀ (x y : α), f (x + y) = f x + f y) :
{to_fun := f, map_one' := h₁, map_mul' := h₂, map_zero' := h₃, map_add' := h₄} = f
theorem ring_hom.coe_add_monoid_hom_injective {α : Type u} {β : Type v} {rα : non_assoc_semiring α} {rβ : non_assoc_semiring β} :
theorem ring_hom.coe_monoid_hom_injective {α : Type u} {β : Type v} {rα : non_assoc_semiring α} {rβ : non_assoc_semiring β} :
@[protected]
theorem ring_hom.map_zero {α : Type u} {β : Type v} {rα : non_assoc_semiring α} {rβ : non_assoc_semiring β} (f : α →+* β) :
f 0 = 0

Ring homomorphisms map zero to zero.

@[protected]
theorem ring_hom.map_one {α : Type u} {β : Type v} {rα : non_assoc_semiring α} {rβ : non_assoc_semiring β} (f : α →+* β) :
f 1 = 1

Ring homomorphisms map one to one.

@[protected]
theorem ring_hom.map_add {α : Type u} {β : Type v} {rα : non_assoc_semiring α} {rβ : non_assoc_semiring β} (f : α →+* β) (a b : α) :
f (a + b) = f a + f b

Ring homomorphisms preserve addition.

@[protected]
theorem ring_hom.map_mul {α : Type u} {β : Type v} {rα : non_assoc_semiring α} {rβ : non_assoc_semiring β} (f : α →+* β) (a b : α) :
f (a * b) = (f a) * f b

Ring homomorphisms preserve multiplication.

@[protected]
theorem ring_hom.map_bit0 {α : Type u} {β : Type v} {rα : non_assoc_semiring α} {rβ : non_assoc_semiring β} (f : α →+* β) (a : α) :
f (bit0 a) = bit0 (f a)

Ring homomorphisms preserve bit0.

@[protected]
theorem ring_hom.map_bit1 {α : Type u} {β : Type v} {rα : non_assoc_semiring α} {rβ : non_assoc_semiring β} (f : α →+* β) (a : α) :
f (bit1 a) = bit1 (f a)

Ring homomorphisms preserve bit1.

theorem ring_hom.codomain_trivial_iff_map_one_eq_zero {α : Type u} {β : Type v} {rα : non_assoc_semiring α} {rβ : non_assoc_semiring β} (f : α →+* β) :
0 = 1 f 1 = 0

f : R →+* S has a trivial codomain iff f 1 = 0.

theorem ring_hom.codomain_trivial_iff_range_trivial {α : Type u} {β : Type v} {rα : non_assoc_semiring α} {rβ : non_assoc_semiring β} (f : α →+* β) :
0 = 1 ∀ (x : α), f x = 0

f : R →+* S has a trivial codomain iff it has a trivial range.

theorem ring_hom.codomain_trivial_iff_range_eq_singleton_zero {α : Type u} {β : Type v} {rα : non_assoc_semiring α} {rβ : non_assoc_semiring β} (f : α →+* β) :
0 = 1 set.range f = {0}

f : R →+* S has a trivial codomain iff its range is {0}.

theorem ring_hom.map_one_ne_zero {α : Type u} {β : Type v} {rα : non_assoc_semiring α} {rβ : non_assoc_semiring β} (f : α →+* β) [nontrivial β] :
f 1 0

f : R →+* S doesn't map 1 to 0 if S is nontrivial

theorem ring_hom.domain_nontrivial {α : Type u} {β : Type v} {rα : non_assoc_semiring α} {rβ : non_assoc_semiring β} (f : α →+* β) [nontrivial β] :

If there is a homomorphism f : R →+* S and S is nontrivial, then R is nontrivial.

theorem ring_hom.is_unit_map {α : Type u} {β : Type v} [semiring α] [semiring β] (f : α →+* β) {a : α} (h : is_unit a) :
def ring_hom.id (α : Type u_1) [non_assoc_semiring α] :
α →+* α

The identity ring homomorphism from a semiring to itself.

Equations
@[protected, instance]
def ring_hom.inhabited {α : Type u} [rα : non_assoc_semiring α] :
Equations
@[simp]
theorem ring_hom.id_apply {α : Type u} [rα : non_assoc_semiring α] (x : α) :
(ring_hom.id α) x = x
@[simp]
@[simp]
theorem ring_hom.coe_monoid_hom_id {α : Type u} [rα : non_assoc_semiring α] :
def ring_hom.comp {α : Type u} {β : Type v} {γ : Type w} [rα : non_assoc_semiring α] [rβ : non_assoc_semiring β] {rγ : non_assoc_semiring γ} (hnp : β →+* γ) (hmn : α →+* β) :
α →+* γ

Composition of ring homomorphisms is a ring homomorphism.

Equations
theorem ring_hom.comp_assoc {α : Type u} {β : Type v} {γ : Type w} [rα : non_assoc_semiring α] [rβ : non_assoc_semiring β] {rγ : non_assoc_semiring γ} {δ : Type u_1} {rδ : non_assoc_semiring δ} (f : α →+* β) (g : β →+* γ) (h : γ →+* δ) :
(h.comp g).comp f = h.comp (g.comp f)

Composition of semiring homomorphisms is associative.

@[simp]
theorem ring_hom.coe_comp {α : Type u} {β : Type v} {γ : Type w} [rα : non_assoc_semiring α] [rβ : non_assoc_semiring β] {rγ : non_assoc_semiring γ} (hnp : β →+* γ) (hmn : α →+* β) :
(hnp.comp hmn) = hnp hmn
theorem ring_hom.comp_apply {α : Type u} {β : Type v} {γ : Type w} [rα : non_assoc_semiring α] [rβ : non_assoc_semiring β] {rγ : non_assoc_semiring γ} (hnp : β →+* γ) (hmn : α →+* β) (x : α) :
(hnp.comp hmn) x = hnp (hmn x)
@[simp]
theorem ring_hom.comp_id {α : Type u} {β : Type v} [rα : non_assoc_semiring α] [rβ : non_assoc_semiring β] (f : α →+* β) :
f.comp (ring_hom.id α) = f
@[simp]
theorem ring_hom.id_comp {α : Type u} {β : Type v} [rα : non_assoc_semiring α] [rβ : non_assoc_semiring β] (f : α →+* β) :
(ring_hom.id β).comp f = f
@[protected, instance]
def ring_hom.monoid {α : Type u} [rα : non_assoc_semiring α] :
monoid →+* α)
Equations
theorem ring_hom.one_def {α : Type u} [rα : non_assoc_semiring α] :
@[simp]
theorem ring_hom.coe_one {α : Type u} [rα : non_assoc_semiring α] :
theorem ring_hom.mul_def {α : Type u} [rα : non_assoc_semiring α] (f g : α →+* α) :
f * g = f.comp g
@[simp]
theorem ring_hom.coe_mul {α : Type u} [rα : non_assoc_semiring α] (f g : α →+* α) :
f * g = f g
theorem ring_hom.cancel_right {α : Type u} {β : Type v} {γ : Type w} [rα : non_assoc_semiring α] [rβ : non_assoc_semiring β] {rγ : non_assoc_semiring γ} {g₁ g₂ : β →+* γ} {f : α →+* β} (hf : function.surjective f) :
g₁.comp f = g₂.comp f g₁ = g₂
theorem ring_hom.cancel_left {α : Type u} {β : Type v} {γ : Type w} [rα : non_assoc_semiring α] [rβ : non_assoc_semiring β] {rγ : non_assoc_semiring γ} {g : β →+* γ} {f₁ f₂ : α →+* β} (hg : function.injective g) :
g.comp f₁ = g.comp f₂ f₁ = f₂
@[simp]
theorem two_dvd_bit0 {α : Type u} [semiring α] {a : α} :
2 bit0 a
theorem ring_hom.map_dvd {α : Type u} {β : Type v} [semiring α] [semiring β] (f : α →+* β) {a b : α} :
a bf a f b
@[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 : α), comm_semiring.nsmul 0 x = 0) . "try_refl_tac"
  • nsmul_succ' : (∀ (n : ) (x : α), comm_semiring.nsmul n.succ x = x + 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
  • one : α
  • one_mul : ∀ (a : α), 1 * a = a
  • mul_one : ∀ (a : α), a * 1 = a
  • npow : α → α
  • npow_zero' : (∀ (x : α), comm_semiring.npow 0 x = 1) . "try_refl_tac"
  • npow_succ' : (∀ (n : ) (x : α), comm_semiring.npow n.succ x = x * comm_semiring.npow n 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
@[instance]
def comm_semiring.to_comm_monoid (α : Type u) [self : comm_semiring α] :
@[instance]
def comm_semiring.to_semiring (α : Type u) [self : comm_semiring α] :
@[protected]
def function.injective.comm_semiring {α : Type u} {γ : Type w} [comm_semiring α] [has_zero γ] [has_one γ] [has_add γ] [has_mul γ] (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) :

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

Equations
@[protected]
def function.surjective.comm_semiring {α : Type u} {γ : Type w} [comm_semiring α] [has_zero γ] [has_one γ] [has_add γ] [has_mul γ] (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) :

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
theorem has_dvd.dvd.linear_comb {α : Type u} [comm_semiring α] {d x y : α} (hdx : d x) (hdy : d y) (a b : α) :
d a * x + b * y

Rings #

@[instance]
def ring.to_add_comm_group (α : Type u) [self : ring α] :
@[instance]
def ring.to_monoid (α : 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
  • mul : α → α → α
  • mul_assoc : ∀ (a b c : α), (a * b) * c = a * b * c
  • one : α
  • 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
@[instance]
def ring.to_distrib (α : Type u) [self : ring α] :
@[protected, instance]
def ring.to_semiring {α : Type u} [ring α] :
Equations
@[protected]
def function.injective.ring {α : Type u} {β : Type v} [ring α] [has_zero β] [has_one β] [has_add β] [has_mul β] [has_neg β] [has_sub β] (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) :
ring β

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

Equations
@[protected]
def function.surjective.ring {α : Type u} {β : Type v} [ring α] [has_zero β] [has_one β] [has_add β] [has_mul β] [has_neg β] [has_sub β] (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) :
ring β

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

Equations
theorem neg_mul_eq_neg_mul {α : Type u} [ring α] (a b : α) :
-a * b = (-a) * b
theorem neg_mul_eq_mul_neg {α : Type u} [ring α] (a b : α) :
-a * b = a * -b
@[simp]
theorem neg_mul_eq_neg_mul_symm {α : Type u} [ring α] (a b : α) :
(-a) * b = -a * b
@[simp]
theorem mul_neg_eq_neg_mul_symm {α : Type u} [ring α] (a b : α) :
a * -b = -a * b
theorem neg_mul_neg {α : Type u} [ring α] (a b : α) :
(-a) * -b = a * b
theorem neg_mul_comm {α : Type u} [ring α] (a b : α) :
(-a) * b = a * -b
theorem neg_eq_neg_one_mul {α : Type u} [ring α] (a : α) :
-a = (-1) * a
theorem mul_sub_left_distrib {α : Type u} [ring α] (a b c : α) :
a * (b - c) = a * b - a * c
theorem mul_sub {α : Type u} [ring α] (a b c : α) :
a * (b - c) = a * b - a * c

Alias of mul_sub_left_distrib.

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

Alias of mul_sub_right_distrib.

theorem mul_neg_one {α : Type u} [ring α] (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} [ring α] (a : α) :
(-1) * a = -a

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

theorem mul_add_eq_mul_add_iff_sub_mul_add_eq {α : Type u} [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} [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.

@[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 : units α) :

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, simp]
theorem units.neg_inv {α : Type u} [ring α] (u : units α) :

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

@[protected, simp]
theorem units.neg_neg {α : Type u} [ring α] (u : units α) :
--u = u

An element of a ring's unit group equals the additive inverse of its additive inverse.

@[protected, simp]
theorem units.neg_mul {α : Type u} [ring α] (u₁ u₂ : units α) :
(-u₁) * u₂ = -u₁ * u₂

Multiplication of elements of a ring's unit group commutes with mapping the first argument to its additive inverse.

@[protected, simp]
theorem units.mul_neg {α : Type u} [ring α] (u₁ u₂ : units α) :
u₁ * -u₂ = -u₁ * u₂

Multiplication of elements of a ring's unit group commutes with mapping the second argument to its additive inverse.

@[protected, simp]
theorem units.neg_mul_neg {α : Type u} [ring α] (u₁ u₂ : units α) :
(-u₁) * -u₂ = u₁ * u₂

Multiplication of the additive inverses of two elements of a ring's unit group equals multiplication of the two original elements.

@[protected]
theorem units.neg_eq_neg_one_mul {α : Type u} [ring α] (u : units α) :
-u = (-1) * u

The additive inverse of an element of a ring's unit group equals the additive inverse of one times the original element.

theorem is_unit.neg {α : Type u} [ring α] {a : α} :
is_unit ais_unit (-a)
theorem is_unit.neg_iff {α : Type u} [ring α] (a : α) :
@[protected]
theorem ring_hom.map_neg {α : Type u_1} {β : Type u_2} [ring α] [ring β] (f : α →+* β) (x : α) :
f (-x) = -f x

Ring homomorphisms preserve additive inverse.

@[protected]
theorem ring_hom.map_sub {α : Type u_1} {β : Type u_2} [ring α] [ring β] (f : α →+* β) (x y : α) :
f (x - y) = f x - f y

Ring homomorphisms preserve subtraction.

theorem ring_hom.injective_iff {α : Type u_1} {β : Type u_2} [ring α] [non_assoc_semiring β] (f : α →+* β) :
function.injective f ∀ (a : α), f a = 0a = 0

A ring homomorphism is injective iff its kernel is trivial.

theorem ring_hom.injective_iff' {α : Type u_1} {β : Type u_2} [ring α] [non_assoc_semiring β] (f : α →+* β) :
function.injective f ∀ (a : α), f a = 0 a = 0

A ring homomorphism is injective iff its kernel is trivial.

def ring_hom.mk' {α : Type u} {γ : Type u_1} [non_assoc_semiring α] [ring γ] (f : α →* γ) (map_add : ∀ (a b : α), f (a + b) = f a + f b) :
α →+* γ

Makes a ring homomorphism from a monoid homomorphism of rings which preserves addition.

Equations
@[instance]
def comm_ring.to_ring (α : Type u) [self : comm_ring α] :
ring α
@[class]
structure comm_ring (α : Type u) :
Type u

A commutative ring is a ring with commutative multiplication.

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

An element a of a ring divides the additive inverse of an element b iff a divides b.

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

The additive inverse of an element a of a ring divides another element b iff a divides b.

theorem dvd_sub {α : Type u} [ring α] {a b c : α} (h₁ : a b) (h₂ : a c) :
a b - c
theorem dvd_add_iff_left {α : Type u} [ring α] {a b c : α} (h : a c) :
a b a b + c
theorem dvd_add_iff_right {α : Type u} [ring α] {a b c : α} (h : a b) :
a c a b + c
theorem two_dvd_bit1 {α : Type u} [ring α] {a : α} :
2 bit1 a 2 1
theorem dvd_add_left {α : Type u} [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} [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.

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

theorem dvd_iff_dvd_of_dvd_sub {α : Type u} [ring α] {a b c : α} (h : a b - c) :
a b a c
@[simp]
theorem even_neg {α : Type u} [ring α] (a : α) :
even (-a) even a
theorem odd.neg {α : Type u} [ring α] {a : α} (hp : odd a) :
odd (-a)
@[simp]
theorem odd_neg {α : Type u} [ring α] (a : α) :
odd (-a) odd a
@[protected]
def function.injective.comm_ring {α : Type u} {β : Type v} [comm_ring α] [has_zero β] [has_one β] [has_add β] [has_mul β] [has_neg β] [has_sub β] (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) :

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

Equations
@[protected]
def function.surjective.comm_ring {α : Type u} {β : Type v} [comm_ring α] [has_zero β] [has_one β] [has_add β] [has_mul β] [has_neg β] [has_sub β] (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) :

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

Equations
theorem mul_self_sub_mul_self {α : Type u} [comm_ring α] (a b : α) :
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 {α : Type u} [comm_ring α] (a : α) :
a * a - 1 = (a + 1) * (a - 1)
theorem Vieta_formula_quadratic {α : Type u} [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} [comm_ring α] {k a b x y : α} (hab : k a - b) (hxy : k x - y) :
k a * x - b * y
theorem succ_ne_self {α : Type u} [ring α] [nontrivial α] (a : α) :
a + 1 a
theorem pred_ne_self {α : Type u} [ring α] [nontrivial α] (a : α) :
a - 1 a
theorem is_left_regular_of_non_zero_divisor {α : Type u} [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} [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} [ring α] [no_zero_divisors α] {k : α} (hk : k 0) :
@[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
@[instance]
def is_domain.to_nontrivial (α : Type u) [ring α] [self : is_domain α] :
@[protected]
theorem function.injective.is_domain {α : Type u} {β : Type v} [ring α] [is_domain α] [ring β] (f : β →+* α) (hf : function.injective f) :

Pullback an is_domain instance along an injective function.

theorem mul_self_eq_mul_self_iff {α : Type u} [comm_ring α] [is_domain α] {a b : α} :
a * a = b * b a = b a = -b
theorem mul_self_eq_one_iff {α : Type u} [comm_ring α] [is_domain α] {a : α} :
a * a = 1 a = 1 a = -1
theorem units.inv_eq_self_iff {α : Type u} [comm_ring α] [is_domain α] (u : units α) :
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.

def add_monoid_hom.mk_ring_hom_of_mul_self_of_two_ne_zero {α : Type u} {β : Type v} [comm_ring α] [is_domain α] [comm_ring β] (f : β →+ α) (h : ∀ (x : β), f (x * x) = (f x) * f x) (h_two : 2 0) (h_one : f 1 = 1) :
β →+* α

Makes a ring homomorphism from an additive group homomorphism from a commutative ring to an integral domain that commutes with self multiplication, assumes that two is nonzero and one is sent to one.

Equations
@[simp]
theorem add_monoid_hom.coe_fn_mk_ring_hom_of_mul_self_of_two_ne_zero {α : Type u} {β : Type v} [comm_ring α] [is_domain α] [comm_ring β] (f : β →+ α) (h : ∀ (x : β), f (x * x) = (f x) * f x) (h_two : 2 0) (h_one : f 1 = 1) :
@[simp]
theorem add_monoid_hom.coe_add_monoid_hom_mk_ring_hom_of_mul_self_of_two_ne_zero {α : Type u} {β : Type v} [comm_ring α] [is_domain α] [comm_ring β] (f : β →+ α) (h : ∀ (x : β), f (x * x) = (f x) * f x) (h_two : 2 0) (h_one : f 1 = 1) :
@[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} [ring 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} [ring R] {a x y : R} :
semiconj_by a (-x) (-y) semiconj_by a x y
theorem semiconj_by.neg_left {R : Type x} [ring 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} [ring R] {a x y : R} :
@[simp]
theorem semiconj_by.neg_one_right {R : Type x} [ring R] (a : R) :
semiconj_by a (-1) (-1)
@[simp]
theorem semiconj_by.neg_one_left {R : Type x} [ring R] (x : R) :
semiconj_by (-1) x x
@[simp]
theorem semiconj_by.sub_right {R : Type x} [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} [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} [semiring R] {x y : R} (h : commute x y) :
theorem commute.bit1_left {R : Type x} [semiring R] {x y : R} (h : commute x y) :
theorem commute.neg_right {R : Type x} [ring R] {a b : R} :
commute a bcommute a (-b)
@[simp]
theorem commute.neg_right_iff {R : Type x} [ring R] {a b : R} :
commute a (-b) commute a b
theorem commute.neg_left {R : Type x} [ring R] {a b : R} :
commute a bcommute (-a) b
@[simp]
theorem commute.neg_left_iff {R : Type x} [ring R] {a b : R} :
commute (-a) b commute a b
@[simp]
theorem commute.neg_one_right {R : Type x} [ring R] (a : R) :
commute a (-1)
@[simp]
theorem commute.neg_one_left {R : Type x} [ring R] (a : R) :
commute (-1) a
@[simp]
theorem commute.sub_right {R : Type x} [ring R] {a b c : R} :
commute a bcommute a ccommute a (b - c)
@[simp]
theorem commute.sub_left {R : Type x} [ring R] {a b c : R} :
commute a ccommute b ccommute (a - b) c