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, integral_domain

Notations

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

Implementation notes

There's a coercion from bundled homs to fun, and the canonical notation is to use the bundled hom as a function via this coercion.

There is no semiring_hom -- the idea is that ring_hom is used. The constructor for a ring_hom between semirings needs a proof of map_zero, map_one and map_add as well as map_mul; a separate constructor ring_hom.mk' will construct ring homs between rings from monoid homs given only a proof that addition is preserved.

Throughout the section on ring_hom implicit {} brackets are often used instead of type class [] brackets. This is done when the instances can be inferred because they are implicit arguments to the type ring_hom. When they can be inferred from the type it is faster to use this method than to use type class inference.

Tags

ring_hom, semiring_hom, semiring, comm_semiring, ring, comm_ring, domain, integral_domain, nonzero, units

distrib class

@[instance]
def distrib.to_has_mul (R : Type u_1) [s : distrib R] :

@[class]
structure distrib  :
Type u_1Type u_1
  • mul : R → R → R
  • add : R → R → R
  • left_distrib : ∀ (a b c_1 : R), a * (b + c_1) = a * b + a * c_1
  • right_distrib : ∀ (a b c_1 : R), (a + b) * c_1 = a * c_1 + b * c_1

A typeclass stating that multiplication is left and right distributive over addition.

Instances
@[instance]
def distrib.to_has_add (R : Type u_1) [s : distrib R] :

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

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

def function.injective.distrib {R : Type x} {S : Type u_1} [has_mul R] [has_add R] [distrib S] (f : R → S) :
function.injective f(∀ (x y : R), f (x + y) = f x + f y)(∀ (x y : R), f (x * y) = (f x) * f y)distrib R

Pullback a distrib instance along an injective function.

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

Pushforward a distrib instance along a surjective function.

Equations

Semirings

@[instance]
def semiring.to_add_comm_monoid (α : Type u) [s : semiring α] :

@[instance]
def semiring.to_distrib (α : Type u) [s : semiring α] :

@[class]
structure semiring  :
Type uType u
  • add : α → α → α
  • add_assoc : ∀ (a b c_1 : α), a + b + c_1 = a + (b + c_1)
  • zero : α
  • zero_add : ∀ (a : α), 0 + a = a
  • add_zero : ∀ (a : α), a + 0 = a
  • add_comm : ∀ (a b : α), a + b = b + a
  • mul : α → α → α
  • mul_assoc : ∀ (a b c_1 : α), (a * b) * c_1 = a * b * c_1
  • one : α
  • one_mul : ∀ (a : α), 1 * a = a
  • mul_one : ∀ (a : α), a * 1 = a
  • zero_mul : ∀ (a : α), 0 * a = 0
  • mul_zero : ∀ (a : α), a * 0 = 0
  • left_distrib : ∀ (a b c_1 : α), a * (b + c_1) = a * b + a * c_1
  • right_distrib : ∀ (a b c_1 : α), (a + b) * c_1 = a * c_1 + b * c_1

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_monoid_with_zero (α : Type u) [s : semiring α] :

def function.injective.semiring {α : Type u} {β : Type v} [semiring α] [has_zero β] [has_one β] [has_add β] [has_mul β] (f : β → α) :
function.injective ff 0 = 0f 1 = 1(∀ (x y : β), f (x + y) = f x + f y)(∀ (x y : β), f (x * y) = (f x) * f y)semiring β

Pullback a semiring instance along an injective function.

Equations
def function.surjective.semiring {α : Type u} {β : Type v} [semiring α] [has_zero β] [has_one β] [has_add β] [has_mul β] (f : α → β) :
function.surjective ff 0 = 0f 1 = 1(∀ (x y : α), f (x + y) = f x + f y)(∀ (x y : α), f (x * y) = (f x) * f y)semiring β

Pullback a semiring instance along an injective function.

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} [semiring α] (P : Prop) [decidable P] (a : α) :
a * ite P 1 0 = ite P a 0

@[simp]
theorem boole_mul {α : Type u_1} [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 α] :
α → 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

def odd {α : Type u} [semiring α] :
α → 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
def add_monoid_hom.mul_left {R : Type u_1} [semiring 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} [semiring R] (r : R) :

def add_monoid_hom.mul_right {R : Type u_1} [semiring R] :
R → R →+ R

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

Equations
@[simp]
theorem add_monoid_hom.mul_right_apply {R : Type u_1} [semiring R] (a r : R) :

def ring_hom.to_add_monoid_hom {α : Type u_1} {β : Type u_2} [semiring α] [semiring β] :
→+* β)α →+ β

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} [semiring α] [semiring β] :
→+* β)α →* β

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) [semiring α] [semiring β] :
Type (max u_1 u_2)

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

@[instance]
def ring_hom.has_coe_to_fun {α : Type u} {β : Type v} {rα : semiring α} {rβ : semiring β} :

Equations
@[simp]
theorem ring_hom.to_fun_eq_coe {α : Type u} {β : Type v} {rα : semiring α} {rβ : semiring β} (f : α →+* β) :

@[simp]
theorem ring_hom.coe_mk {α : Type u} {β : Type v} {rα : semiring α} {rβ : 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

@[instance]
def ring_hom.has_coe_monoid_hom {α : Type u} {β : Type v} {rα : semiring α} {rβ : semiring β} :
has_coe →+* β) →* β)

Equations
@[simp]
theorem ring_hom.coe_monoid_hom {α : Type u} {β : Type v} {rα : semiring α} {rβ : semiring β} (f : α →+* β) :

@[simp]
theorem ring_hom.to_monoid_hom_eq_coe {α : Type u} {β : Type v} {rα : semiring α} {rβ : semiring β} (f : α →+* β) :

@[simp]
theorem ring_hom.coe_monoid_hom_mk {α : Type u} {β : Type v} {rα : semiring α} {rβ : 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₂}

@[instance]
def ring_hom.has_coe_add_monoid_hom {α : Type u} {β : Type v} {rα : semiring α} {rβ : semiring β} :
has_coe →+* β) →+ β)

Equations
@[simp]
theorem ring_hom.coe_add_monoid_hom {α : Type u} {β : Type v} {rα : semiring α} {rβ : semiring β} (f : α →+* β) :

@[simp]
theorem ring_hom.to_add_monoid_hom_eq_coe {α : Type u} {β : Type v} {rα : semiring α} {rβ : semiring β} (f : α →+* β) :

@[simp]
theorem ring_hom.coe_add_monoid_hom_mk {α : Type u} {β : Type v} {rα : semiring α} {rβ : 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α : semiring α} {rβ : semiring β} {f g : α →+* β} (h : f = g) (x : α) :
f x = g x

theorem ring_hom.congr_arg {α : Type u} {β : Type v} {rα : semiring α} {rβ : semiring β} (f : α →+* β) {x y : α} :
x = yf x = f y

theorem ring_hom.coe_inj {α : Type u} {β : Type v} {rα : semiring α} {rβ : semiring β} ⦃f g : α →+* β⦄ :
f = gf = g

@[ext]
theorem ring_hom.ext {α : Type u} {β : Type v} {rα : semiring α} {rβ : semiring β} ⦃f g : α →+* β⦄ :
(∀ (x : α), f x = g x)f = g

theorem ring_hom.ext_iff {α : Type u} {β : Type v} {rα : semiring α} {rβ : semiring β} {f g : α →+* β} :
f = g ∀ (x : α), f x = g x

theorem ring_hom.coe_add_monoid_hom_injective {α : Type u} {β : Type v} {rα : semiring α} {rβ : semiring β} :

theorem ring_hom.coe_monoid_hom_injective {α : Type u} {β : Type v} {rα : semiring α} {rβ : semiring β} :

@[simp]
theorem ring_hom.map_zero {α : Type u} {β : Type v} {rα : semiring α} {rβ : semiring β} (f : α →+* β) :
f 0 = 0

Ring homomorphisms map zero to zero.

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

Ring homomorphisms map one to one.

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

Ring homomorphisms preserve addition.

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

Ring homomorphisms preserve multiplication.

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

Ring homomorphisms preserve bit0.

@[simp]
theorem ring_hom.map_bit1 {α : Type u} {β : Type v} {rα : semiring α} {rβ : 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α : semiring α} {rβ : 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α : semiring α} {rβ : 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α : semiring α} {rβ : 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α : semiring α} {rβ : 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α : semiring α} {rβ : 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} {rα : semiring α} {rβ : semiring β} (f : α →+* β) {a : α} :
is_unit ais_unit (f a)

def ring_hom.id (α : Type u_1) [semiring α] :
α →+* α

The identity ring homomorphism from a semiring to itself.

Equations
@[instance]
def ring_hom.inhabited {α : Type u} [rα : semiring α] :

Equations
@[simp]
theorem ring_hom.id_apply {α : Type u} [rα : semiring α] (x : α) :
(ring_hom.id α) x = x

def ring_hom.comp {α : Type u} {β : Type v} {γ : Type w} [rα : semiring α] [rβ : semiring β] {rγ : semiring γ} :
→+* γ)→+* β)α →+* γ

Composition of ring homomorphisms is a ring homomorphism.

Equations
theorem ring_hom.comp_assoc {α : Type u} {β : Type v} {γ : Type w} [rα : semiring α] [rβ : semiring β] {rγ : semiring γ} {δ : Type u_1} {rδ : 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α : semiring α] [rβ : semiring β] {rγ : semiring γ} (hnp : β →+* γ) (hmn : α →+* β) :
(hnp.comp hmn) = hnp hmn

theorem ring_hom.comp_apply {α : Type u} {β : Type v} {γ : Type w} [rα : semiring α] [rβ : semiring β] {rγ : semiring γ} (hnp : β →+* γ) (hmn : α →+* β) (x : α) :
(hnp.comp hmn) x = hnp (hmn x)

@[simp]
theorem ring_hom.comp_id {α : Type u} {β : Type v} [rα : semiring α] [rβ : semiring β] (f : α →+* β) :
f.comp (ring_hom.id α) = f

@[simp]
theorem ring_hom.id_comp {α : Type u} {β : Type v} [rα : semiring α] [rβ : semiring β] (f : α →+* β) :
(ring_hom.id β).comp f = f

@[instance]
def ring_hom.monoid {α : Type u} [rα : semiring α] :
monoid →+* α)

Equations
theorem ring_hom.one_def {α : Type u} [rα : semiring α] :

@[simp]
theorem ring_hom.coe_one {α : Type u} [rα : semiring α] :

theorem ring_hom.mul_def {α : Type u} [rα : semiring α] (f g : α →+* α) :
f * g = f.comp g

@[simp]
theorem ring_hom.coe_mul {α : Type u} [rα : semiring α] (f g : α →+* α) :
f * g = f g

theorem ring_hom.cancel_right {α : Type u} {β : Type v} {γ : Type w} [rα : semiring α] [rβ : semiring β] {rγ : semiring γ} {g₁ g₂ : β →+* γ} {f : α →+* β} :
function.surjective f(g₁.comp f = g₂.comp f g₁ = g₂)

theorem ring_hom.cancel_left {α : Type u} {β : Type v} {γ : Type w} [rα : semiring α] [rβ : semiring β] {rγ : semiring γ} {g : β →+* γ} {f₁ f₂ : α →+* β} :
function.injective g(g.comp f₁ = g.comp f₂ f₁ = f₂)

@[class]
structure comm_semiring  :
Type uType u
  • add : α → α → α
  • add_assoc : ∀ (a b c_1 : α), a + b + c_1 = a + (b + c_1)
  • zero : α
  • zero_add : ∀ (a : α), 0 + a = a
  • add_zero : ∀ (a : α), a + 0 = a
  • add_comm : ∀ (a b : α), a + b = b + a
  • mul : α → α → α
  • mul_assoc : ∀ (a b c_1 : α), (a * b) * c_1 = a * b * c_1
  • one : α
  • one_mul : ∀ (a : α), 1 * a = a
  • mul_one : ∀ (a : α), a * 1 = a
  • zero_mul : ∀ (a : α), 0 * a = 0
  • mul_zero : ∀ (a : α), a * 0 = 0
  • left_distrib : ∀ (a b c_1 : α), a * (b + c_1) = a * b + a * c_1
  • right_distrib : ∀ (a b c_1 : α), (a + b) * c_1 = a * c_1 + b * c_1
  • 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) [s : comm_semiring α] :

@[instance]
def comm_semiring.to_semiring (α : Type u) [s : comm_semiring α] :

def function.injective.comm_semiring {α : Type u} {γ : Type w} [comm_semiring α] [has_zero γ] [has_one γ] [has_add γ] [has_mul γ] (f : γ → α) :
function.injective ff 0 = 0f 1 = 1(∀ (x y : γ), f (x + y) = f x + f y)(∀ (x y : γ), f (x * y) = (f x) * f y)comm_semiring γ

Pullback a semiring instance along an injective function.

Equations
def function.surjective.comm_semiring {α : Type u} {γ : Type w} [comm_semiring α] [has_zero γ] [has_one γ] [has_add γ] [has_mul γ] (f : α → γ) :
function.surjective ff 0 = 0f 1 = 1(∀ (x y : α), f (x + y) = f x + f y)(∀ (x y : α), f (x * y) = (f x) * f y)comm_semiring γ

Pullback a semiring instance along an injective function.

Equations
theorem add_mul_self_eq {α : Type u} [comm_semiring α] (a b : α) :
(a + b) * (a + b) = a * a + (2 * a) * b + b * b

theorem dvd_add {α : Type u} [comm_semiring α] {a b c : α} :
a ba ca b + c

@[simp]
theorem two_dvd_bit0 {α : Type u} [comm_semiring α] {a : α} :
2 bit0 a

theorem ring_hom.map_dvd {α : Type u} {β : Type v} [comm_semiring α] [comm_semiring β] (f : α →+* β) {a b : α} :
a bf a f b

Rings

@[instance]
def ring.to_add_comm_group (α : Type u) [s : ring α] :

@[instance]
def ring.to_monoid (α : Type u) [s : ring α] :

@[class]
structure ring  :
Type uType u
  • add : α → α → α
  • add_assoc : ∀ (a b c_1 : α), a + b + c_1 = a + (b + c_1)
  • zero : α
  • zero_add : ∀ (a : α), 0 + a = a
  • add_zero : ∀ (a : α), a + 0 = a
  • neg : α → α
  • add_left_neg : ∀ (a : α), -a + a = 0
  • add_comm : ∀ (a b : α), a + b = b + a
  • mul : α → α → α
  • mul_assoc : ∀ (a b c_1 : α), (a * b) * c_1 = a * b * c_1
  • one : α
  • one_mul : ∀ (a : α), 1 * a = a
  • mul_one : ∀ (a : α), a * 1 = a
  • left_distrib : ∀ (a b c_1 : α), a * (b + c_1) = a * b + a * c_1
  • right_distrib : ∀ (a b c_1 : α), (a + b) * c_1 = a * c_1 + b * c_1

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) [s : ring α] :

@[instance]
def ring.to_semiring {α : Type u} [ring α] :

Equations
def function.injective.ring {α : Type u} {β : Type v} [ring α] [has_zero β] [has_one β] [has_add β] [has_mul β] [has_neg β] (f : β → α) :
function.injective ff 0 = 0f 1 = 1(∀ (x y : β), f (x + y) = f x + f y)(∀ (x y : β), f (x * y) = (f x) * f y)(∀ (x : β), f (-x) = -f x)ring β

Pullback a ring instance along an injective function.

Equations
def function.surjective.ring {α : Type u} {β : Type v} [ring α] [has_zero β] [has_one β] [has_add β] [has_mul β] [has_neg β] (f : α → β) :
function.surjective ff 0 = 0f 1 = 1(∀ (x y : α), f (x + y) = f x + f y)(∀ (x y : α), f (x * y) = (f x) * f y)(∀ (x : α), f (-x) = -f x)ring β

Pullback a ring instance along an injective function.

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_right_distrib {α : Type u} [ring α] (a b c : α) :
(a - b) * c = a * c - b * c

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.

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

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

Equations
@[simp]
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.

@[simp]
theorem units.coe_neg_one {α : Type u} [ring α] :
-1 = -1

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

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

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

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

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

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.

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

Ring homomorphisms preserve additive inverse.

@[simp]
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 α] [semiring β] (f : α →+* β) :
function.injective f ∀ (a : α), f a = 0a = 0

A ring homomorphism is injective iff its kernel is trivial.

def ring_hom.mk' {α : Type u} {γ : Type u_1} [semiring α] [ring γ] (f : α →* γ) :
(∀ (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) [s : comm_ring α] :
ring α

@[class]
structure comm_ring  :
Type uType u
  • add : α → α → α
  • add_assoc : ∀ (a b c_1 : α), a + b + c_1 = a + (b + c_1)
  • zero : α
  • zero_add : ∀ (a : α), 0 + a = a
  • add_zero : ∀ (a : α), a + 0 = a
  • neg : α → α
  • add_left_neg : ∀ (a : α), -a + a = 0
  • add_comm : ∀ (a b : α), a + b = b + a
  • mul : α → α → α
  • mul_assoc : ∀ (a b c_1 : α), (a * b) * c_1 = a * b * c_1
  • one : α
  • one_mul : ∀ (a : α), 1 * a = a
  • mul_one : ∀ (a : α), a * 1 = a
  • left_distrib : ∀ (a b c_1 : α), a * (b + c_1) = a * b + a * c_1
  • right_distrib : ∀ (a b c_1 : α), (a + b) * c_1 = a * c_1 + b * c_1
  • mul_comm : ∀ (a b : α), a * b = b * a

A commutative ring is a ring with commutative multiplication.

Instances
@[instance]
def comm_ring.to_comm_semigroup (α : Type u) [s : comm_ring α] :

@[instance]
def comm_ring.to_comm_semiring {α : Type u} [s : comm_ring α] :

Equations
def function.injective.comm_ring {α : Type u} {β : Type v} [comm_ring α] [has_zero β] [has_one β] [has_add β] [has_mul β] [has_neg β] (f : β → α) :
function.injective ff 0 = 0f 1 = 1(∀ (x y : β), f (x + y) = f x + f y)(∀ (x y : β), f (x * y) = (f x) * f y)(∀ (x : β), f (-x) = -f x)comm_ring β

Pullback a ring instance along an injective function.

Equations
def function.surjective.comm_ring {α : Type u} {β : Type v} [comm_ring α] [has_zero β] [has_one β] [has_add β] [has_mul β] [has_neg β] (f : α → β) :
function.surjective ff 0 = 0f 1 = 1(∀ (x y : α), f (x + y) = f x + f y)(∀ (x y : α), f (x * y) = (f x) * f y)(∀ (x : α), f (-x) = -f x)comm_ring β

Pullback a ring instance along an injective function.

Equations
theorem dvd_neg_of_dvd {α : Type u} [comm_ring α] {a b : α} :
a ba -b

theorem dvd_of_dvd_neg {α : Type u} [comm_ring α] {a b : α} :
a -ba b

theorem dvd_neg_iff_dvd {α : Type u} [comm_ring α] (a b : α) :
a -b a b

theorem neg_dvd_of_dvd {α : Type u} [comm_ring α] {a b : α} :
a b-a b

theorem dvd_of_neg_dvd {α : Type u} [comm_ring α] {a b : α} :
-a ba b

theorem neg_dvd_iff_dvd {α : Type u} [comm_ring α] (a b : α) :
-a b a b

theorem dvd_sub {α : Type u} [comm_ring α] {a b c : α} :
a ba ca b - c

theorem dvd_add_iff_left {α : Type u} [comm_ring α] {a b c : α} :
a c(a b a b + c)

theorem dvd_add_iff_right {α : Type u} [comm_ring α] {a b c : α} :
a b(a c a b + c)

theorem two_dvd_bit1 {α : Type u} [comm_ring α] {a : α} :
2 bit1 a 2 1

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)

@[simp]
theorem dvd_neg {α : Type u} [comm_ring α] (a b : α) :
a -b a b

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

@[simp]
theorem neg_dvd {α : Type u} [comm_ring α] (a b : α) :
-a b a b

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

theorem dvd_add_left {α : Type u} [comm_ring α] {a b c : α} :
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} [comm_ring α] {a b c : α} :
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} [comm_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} [comm_ring α] {a b : α} :
a b + a a b

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

theorem Vieta_formula_quadratic {α : Type u} [comm_ring α] {b c x : α} :
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 : α} :
k a - bk x - yk a * x - b * y

theorem dvd_iff_dvd_of_dvd_sub {α : Type u} [comm_ring α] {a b c : α} :
a b - c(a b a c)

theorem succ_ne_self {α : Type u} [ring α] [nontrivial α] (a : α) :
a + 1 a

theorem pred_ne_self {α : Type u} [ring α] [nontrivial α] (a : α) :
a - 1 a

@[instance]
def domain.to_ring (α : Type u) [s : domain α] :
ring α

@[class]
structure domain  :
Type uType u
  • add : α → α → α
  • add_assoc : ∀ (a b c_1 : α), a + b + c_1 = a + (b + c_1)
  • zero : α
  • zero_add : ∀ (a : α), 0 + a = a
  • add_zero : ∀ (a : α), a + 0 = a
  • neg : α → α
  • add_left_neg : ∀ (a : α), -a + a = 0
  • add_comm : ∀ (a b : α), a + b = b + a
  • mul : α → α → α
  • mul_assoc : ∀ (a b c_1 : α), (a * b) * c_1 = a * b * c_1
  • one : α
  • one_mul : ∀ (a : α), 1 * a = a
  • mul_one : ∀ (a : α), a * 1 = a
  • left_distrib : ∀ (a b c_1 : α), a * (b + c_1) = a * b + a * c_1
  • right_distrib : ∀ (a b c_1 : α), (a + b) * c_1 = a * c_1 + b * c_1
  • exists_pair_ne : ∃ (x y : α), x y
  • eq_zero_or_eq_zero_of_mul_eq_zero : ∀ (a b : α), a * b = 0a = 0 b = 0

A domain is a ring with no zero divisors, i.e. satisfying the condition a * b = 0 ↔ a = 0 ∨ b = 0. Alternatively, a domain is an integral domain without assuming commutativity of multiplication.

Instances
@[instance]
def domain.to_nontrivial (α : Type u) [s : domain α] :

@[instance]
def domain.to_no_zero_divisors {α : Type u} [domain α] :

def function.injective.domain {α : Type u} {β : Type v} [domain α] [has_zero β] [has_one β] [has_add β] [has_mul β] [has_neg β] (f : β → α) :
function.injective ff 0 = 0f 1 = 1(∀ (x y : β), f (x + y) = f x + f y)(∀ (x y : β), f (x * y) = (f x) * f y)(∀ (x : β), f (-x) = -f x)domain β

Pullback a domain instance along an injective function.

Equations

Integral domains

@[class]
structure integral_domain  :
Type uType u
  • add : α → α → α
  • add_assoc : ∀ (a b c_1 : α), a + b + c_1 = a + (b + c_1)
  • zero : α
  • zero_add : ∀ (a : α), 0 + a = a
  • add_zero : ∀ (a : α), a + 0 = a
  • neg : α → α
  • add_left_neg : ∀ (a : α), -a + a = 0
  • add_comm : ∀ (a b : α), a + b = b + a
  • mul : α → α → α
  • mul_assoc : ∀ (a b c_1 : α), (a * b) * c_1 = a * b * c_1
  • one : α
  • one_mul : ∀ (a : α), 1 * a = a
  • mul_one : ∀ (a : α), a * 1 = a
  • left_distrib : ∀ (a b c_1 : α), a * (b + c_1) = a * b + a * c_1
  • right_distrib : ∀ (a b c_1 : α), (a + b) * c_1 = a * c_1 + b * c_1
  • mul_comm : ∀ (a b : α), a * b = b * a
  • exists_pair_ne : ∃ (x y : α), x y
  • eq_zero_or_eq_zero_of_mul_eq_zero : ∀ (a b : α), a * b = 0a = 0 b = 0

An integral domain is a commutative ring with no zero divisors, i.e. satisfying the condition a * b = 0 ↔ a = 0 ∨ b = 0. Alternatively, an integral domain is a domain with commutative multiplication.

Instances
@[instance]
def integral_domain.to_domain (α : Type u) [s : integral_domain α] :

@[instance]
def integral_domain.to_comm_ring (α : Type u) [s : integral_domain α] :

def function.injective.integral_domain {α : Type u} {β : Type v} [integral_domain α] [has_zero β] [has_one β] [has_add β] [has_mul β] [has_neg β] (f : β → α) :
function.injective ff 0 = 0f 1 = 1(∀ (x y : β), f (x + y) = f x + f y)(∀ (x y : β), f (x * y) = (f x) * f y)(∀ (x : β), f (-x) = -f x)integral_domain β

Pullback an integral_domain instance along an injective function.

Equations
theorem mul_self_eq_mul_self_iff {α : Type u} [integral_domain α] {a b : α} :
a * a = b * b a = b a = -b

theorem mul_self_eq_one_iff {α : Type u} [integral_domain α] {a : α} :
a * a = 1 a = 1 a = -1

theorem units.inv_eq_self_iff {α : Type u} [integral_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 ring.inverse {R : Type x} [ring R] :
R → R

Introduce a function inverse on a ring R, which sends x to x⁻¹ if x is invertible and to 0 otherwise. This definition is somewhat ad hoc, but one needs a fully (rather than partially) defined inverse function for some purposes, including for calculus.

Equations
@[simp]
theorem ring.inverse_unit {R : Type x} [ring R] (a : units R) :

By definition, if x is invertible then inverse x = x⁻¹.

@[simp]
theorem ring.inverse_non_unit {R : Type x} [ring R] (x : R) :

By definition, if x is not invertible then inverse x = 0.

@[nolint]

structure is_integral_domain (R : Type u) [ring R] :
Prop
  • exists_pair_ne : ∃ (x y : R), x y
  • mul_comm : ∀ (x y : R), x * y = y * x
  • eq_zero_or_eq_zero_of_mul_eq_zero : ∀ (x y : R), x * y = 0x = 0 y = 0

A predicate to express that a ring is an integral domain.

This is mainly useful because such a predicate does not contain data, and can therefore be easily transported along ring isomorphisms.

Every integral domain satisfies the predicate for integral domains.

If a ring satisfies the predicate for integral domains, then it can be endowed with an integral_domain instance whose data is definitionally equal to the existing data.

Equations
@[simp]
theorem semiconj_by.add_right {R : Type x} [distrib R] {a x y x' y' : R} :
semiconj_by a x ysemiconj_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} :
semiconj_by a x ysemiconj_by b x ysemiconj_by (a + b) x y

theorem semiconj_by.neg_right {R : Type x} [ring R] {a x y : R} :
semiconj_by a x ysemiconj_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} :
semiconj_by a x ysemiconj_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} :
semiconj_by a x ysemiconj_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} :
semiconj_by a x ysemiconj_by b x ysemiconj_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.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