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 #

Tags #

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

distrib class #

source
@[instance]
def distrib.to_has_mul (R : Type u_1) [self : distrib R] :
has_mul R
source
@[class]
structure distrib (R : Type u_1) :
Type u_1
  • mul : R → R → R
  • add : R → R → R
  • left_distrib : ∀ (a b c : R), a * (b + c) = a * b + a * c
  • right_distrib : ∀ (a b c : R), (a + b) * c = a * c + b * c

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

Instances
source
@[instance]
def distrib.to_has_add (R : Type u_1) [self : distrib R] :
has_add R
source
theorem left_distrib {R : Type x} [distrib R] (a b c : R) :
a * (b + c) = a * b + a * c
source
theorem mul_add {R : Type x} [distrib R] (a b c : R) :
a * (b + c) = a * b + a * c

Alias of left_distrib.

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

Alias of right_distrib.

source
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) :
distrib R

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

Equations
source
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) :
distrib S

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

Equations

Semirings #

source
@[instance]
def non_unital_non_assoc_semiring.to_distrib (α : Type u) [self : non_unital_non_assoc_semiring α] :
distrib α
source
@[instance]
def non_unital_non_assoc_semiring.to_mul_zero_class (α : Type u) [self : non_unital_non_assoc_semiring α] :
mul_zero_class α
source
@[instance]
def non_unital_non_assoc_semiring.to_add_comm_monoid (α : Type u) [self : non_unital_non_assoc_semiring α] :
add_comm_monoid α
source
@[class]
structure non_unital_non_assoc_semiring (α : Type u) :
Type u

A not-necessarily-unital, not-necessarily-associative semiring.

Instances
source
@[instance]
def non_unital_semiring.to_semigroup_with_zero (α : Type u) [self : non_unital_semiring α] :
semigroup_with_zero α
source
@[instance]
def non_unital_semiring.to_non_unital_non_assoc_semiring (α : Type u) [self : non_unital_semiring α] :
non_unital_non_assoc_semiring α
source
@[class]
structure non_unital_semiring (α : Type u) :
Type u
  • 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
source
@[instance]
def non_assoc_semiring.to_non_unital_non_assoc_semiring (α : Type u) [self : non_assoc_semiring α] :
non_unital_non_assoc_semiring α
source
@[instance]
def non_assoc_semiring.to_mul_zero_one_class (α : Type u) [self : non_assoc_semiring α] :
mul_zero_one_class α
source
@[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
source
@[instance]
def semiring.to_non_assoc_semiring (α : Type u) [self : semiring α] :
non_assoc_semiring α
source
@[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
source
@[instance]
def semiring.to_non_unital_semiring (α : Type u) [self : semiring α] :
non_unital_semiring α
source
@[instance]
def semiring.to_monoid_with_zero (α : Type u) [self : semiring α] :
monoid_with_zero α
source
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) :
non_unital_non_assoc_semiring β

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

Equations
source
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) :
non_unital_semiring β

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

Equations
source
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) :
non_assoc_semiring β

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

Equations
source
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) :
semiring β

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

Equations
source
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) :
non_unital_non_assoc_semiring β

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

Equations
source
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) :
non_unital_semiring β

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

Equations
source
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) :
non_assoc_semiring β

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

Equations
source
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) :
semiring β

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

Equations
source
theorem one_add_one_eq_two {α : Type u} [semiring α] :
1 + 1 = 2
source
theorem two_mul {α : Type u} [semiring α] (n : α) :
2 * n = n + n
source
theorem distrib_three_right {α : Type u} [semiring α] (a b c d : α) :
(a + b + c) * d = a * d + b * d + c * d
source
theorem mul_two {α : Type u} [semiring α] (n : α) :
n * 2 = n + n
source
theorem bit0_eq_two_mul {α : Type u} [semiring α] (n : α) :
bit0 n = 2 * n
source
theorem add_ite {α : Type u_1} [has_add α] (P : Prop) [decidable P] (a b c : α) :
a + ite P b c = ite P (a + b) (a + c)
source
@[simp]
theorem mul_ite {α : Type u_1} [has_mul α] (P : Prop) [decidable P] (a b c : α) :
a * ite P b c = ite P (a * b) (a * c)
source
theorem ite_add {α : Type u_1} [has_add α] (P : Prop) [decidable P] (a b c : α) :
ite P a b + c = ite P (a + c) (b + c)
source
@[simp]
theorem ite_mul {α : Type u_1} [has_mul α] (P : Prop) [decidable P] (a b c : α) :
(ite P a b) * c = ite P (a * c) (b * c)
source
@[simp]
theorem mul_boole {α : Type u_1} [non_assoc_semiring α] (P : Prop) [decidable P] (a : α) :
a * ite P 1 0 = ite P a 0
source
@[simp]
theorem boole_mul {α : Type u_1} [non_assoc_semiring α] (P : Prop) [decidable P] (a : α) :
(ite P 1 0) * a = ite P a 0
source
theorem ite_mul_zero_left {α : Type u_1} [mul_zero_class α] (P : Prop) [decidable P] (a b : α) :
ite P (a * b) 0 = (ite P a 0) * b
source
theorem ite_mul_zero_right {α : Type u_1} [mul_zero_class α] (P : Prop) [decidable P] (a b : α) :
ite P (a * b) 0 = a * ite P b 0
source
def even {α : Type u} [semiring α] (a : α) :
Prop

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

Equations
source
theorem even_iff_two_dvd {α : Type u} [semiring α] {a : α} :
even a ↔ 2 ∣ a
source
@[simp]
theorem range_two_mul (α : Type u_1) [semiring α] :
set.range (λ (x : α), 2 * x) = {a : α | even a}
source
@[simp]
theorem even_bit0 {α : Type u} [semiring α] (a : α) :
even (bit0 a)
source
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
source
@[simp]
theorem odd_bit1 {α : Type u} [semiring α] (a : α) :
odd (bit1 a)
source
@[simp]
theorem range_two_mul_add_one (α : Type u_1) [semiring α] :
set.range (λ (x : α), 2 * x + 1) = {a : α | odd a}
source
theorem dvd_add {α : Type u} [semiring α] {a b c : α} (h₁ : a ∣ b) (h₂ : a ∣ c) :
a ∣ b + c
source
def add_hom.mul_left {R : Type u_1} [distrib R] (r : R) :
add_hom R R

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

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

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

Equations
source
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
source
@[simp]
theorem add_monoid_hom.coe_mul_left {R : Type u_1} [non_unital_non_assoc_semiring R] (r : R) :
⇑(add_monoid_hom.mul_left r) = has_mul.mul r
source
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
source
@[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
source
theorem add_monoid_hom.mul_right_apply {R : Type u_1} [non_unital_non_assoc_semiring R] (a r : R) :
⇑(add_monoid_hom.mul_right r) a = a * r
source
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).

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

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

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

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

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

source
@[instance]
def ring_hom.has_coe_to_fun {α : Type u} {β : Type v} {rα : non_assoc_semiring α} {rβ : non_assoc_semiring β} :
has_coe_to_fun (α →+* β)
Equations
source
@[simp]
theorem ring_hom.to_fun_eq_coe {α : Type u} {β : Type v} {rα : non_assoc_semiring α} {rβ : non_assoc_semiring β} (f : α →+* β) :
f.to_fun = ⇑f
source
@[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
source
@[instance]
def ring_hom.has_coe_monoid_hom {α : Type u} {β : Type v} {rα : non_assoc_semiring α} {rβ : non_assoc_semiring β} :
has_coe (α →+* β) (α →* β)
Equations
source
@[simp]
theorem ring_hom.coe_monoid_hom {α : Type u} {β : Type v} {rα : non_assoc_semiring α} {rβ : non_assoc_semiring β} (f : α →+* β) :
⇑↑f = ⇑f
source
@[simp]
theorem ring_hom.to_monoid_hom_eq_coe {α : Type u} {β : Type v} {rα : non_assoc_semiring α} {rβ : non_assoc_semiring β} (f : α →+* β) :
f.to_monoid_hom = ↑f
source
@[simp]
theorem ring_hom.to_monoid_with_zero_hom_eq_coe {α : Type u} {β : Type v} {rα : non_assoc_semiring α} {rβ : non_assoc_semiring β} (f : α →+* β) :
⇑(f.to_monoid_with_zero_hom) = ⇑f
source
@[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₂}
source
@[instance]
def ring_hom.has_coe_add_monoid_hom {α : Type u} {β : Type v} {rα : non_assoc_semiring α} {rβ : non_assoc_semiring β} :
has_coe (α →+* β) (α →+ β)
Equations
source
@[simp]
theorem ring_hom.coe_add_monoid_hom {α : Type u} {β : Type v} {rα : non_assoc_semiring α} {rβ : non_assoc_semiring β} (f : α →+* β) :
⇑↑f = ⇑f
source
@[simp]
theorem ring_hom.to_add_monoid_hom_eq_coe {α : Type u} {β : Type v} {rα : non_assoc_semiring α} {rβ : non_assoc_semiring β} (f : α →+* β) :
f.to_add_monoid_hom = ↑f
source
@[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₄}
source
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
source
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
source
theorem ring_hom.coe_inj {α : Type u} {β : Type v} {rα : non_assoc_semiring α} {rβ : non_assoc_semiring β} ⦃f g : α →+* β⦄ (h : ⇑f = ⇑g) :
f = g
source
@[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
source
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
source
@[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
source
theorem ring_hom.coe_add_monoid_hom_injective {α : Type u} {β : Type v} {rα : non_assoc_semiring α} {rβ : non_assoc_semiring β} :
function.injective coe
source
theorem ring_hom.coe_monoid_hom_injective {α : Type u} {β : Type v} {rα : non_assoc_semiring α} {rβ : non_assoc_semiring β} :
function.injective coe
source
@[simp]
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.

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

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

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

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

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

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

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

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

source
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

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

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

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

The identity ring homomorphism from a semiring to itself.

Equations
source
@[instance]
def ring_hom.inhabited {α : Type u} [rα : non_assoc_semiring α] :
inhabited (α →+* α)
Equations
source
@[simp]
theorem ring_hom.id_apply {α : Type u} [rα : non_assoc_semiring α] (x : α) :
⇑(ring_hom.id α) x = x
source
@[simp]
theorem ring_hom.coe_add_monoid_hom_id {α : Type u} [rα : non_assoc_semiring α] :
↑(ring_hom.id α) = add_monoid_hom.id α
source
@[simp]
theorem ring_hom.coe_monoid_hom_id {α : Type u} [rα : non_assoc_semiring α] :
↑(ring_hom.id α) = monoid_hom.id α
source
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
source
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.

source
@[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
source
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)
source
@[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
source
@[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
source
@[instance]
def ring_hom.monoid {α : Type u} [rα : non_assoc_semiring α] :
monoid (α →+* α)
Equations
source
theorem ring_hom.one_def {α : Type u} [rα : non_assoc_semiring α] :
1 = ring_hom.id α
source
@[simp]
theorem ring_hom.coe_one {α : Type u} [rα : non_assoc_semiring α] :
⇑1 = id
source
theorem ring_hom.mul_def {α : Type u} [rα : non_assoc_semiring α] (f g : α →+* α) :
f * g = f.comp g
source
@[simp]
theorem ring_hom.coe_mul {α : Type u} [rα : non_assoc_semiring α] (f g : α →+* α) :
⇑f * g = ⇑f ∘ ⇑g
source
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₂
source
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₂
source
@[simp]
theorem two_dvd_bit0 {α : Type u} [semiring α] {a : α} :
2 ∣ bit0 a
source
theorem ring_hom.map_dvd {α : Type u} {β : Type v} [semiring α] [semiring β] (f : α →+* β) {a b : α} :
a ∣ b → ⇑f a ∣ ⇑f b
source
@[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
source
@[instance]
def comm_semiring.to_comm_monoid (α : Type u) [self : comm_semiring α] :
comm_monoid α
source
@[instance]
def comm_semiring.to_semiring (α : Type u) [self : comm_semiring α] :
semiring α
source
@[instance]
def comm_semiring.to_comm_monoid_with_zero {α : Type u} [comm_semiring α] :
comm_monoid_with_zero α
Equations
source
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) :
comm_semiring γ

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

Equations
source
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) :
comm_semiring γ

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

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

Rings #

source
@[instance]
def ring.to_add_comm_group (α : Type u) [self : ring α] :
add_comm_group α
source
@[instance]
def ring.to_monoid (α : Type u) [self : ring α] :
monoid α
source
@[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"
  • gsmul : ℤ → α → α
  • gsmul_zero' : (∀ (a : α), ring.gsmul 0 a = 0) . "try_refl_tac"
  • gsmul_succ' : (∀ (n : ℕ) (a : α), ring.gsmul (int.of_nat n.succ) a = a + ring.gsmul (int.of_nat n) a) . "try_refl_tac"
  • gsmul_neg' : (∀ (n : ℕ) (a : α), ring.gsmul -[1+ n] a = -ring.gsmul ↑(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
source
@[instance]
def ring.to_distrib (α : Type u) [self : ring α] :
distrib α
source
@[instance]
def ring.to_semiring {α : Type u} [ring α] :
semiring α
Equations
source
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
source
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 β

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

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

Alias of mul_sub_left_distrib.

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

Alias of mul_sub_right_distrib.

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

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

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

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

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

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

Equations
source
@[simp]
theorem units.coe_neg {α : Type u} [ring α] (u : units α) :
↑-u = -↑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.

source
@[simp]
theorem units.coe_neg_one {α : Type u} [ring α] :
↑-1 = -1
source
@[simp]
theorem units.neg_inv {α : Type u} [ring α] (u : units α) :
(-u)⁻¹ = -u⁻¹

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

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

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

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

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

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

source
theorem is_unit.neg {α : Type u} [ring α] {a : α} :
is_unit a → is_unit (-a)
source
@[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.

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

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

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

source
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
source
@[instance]
def comm_ring.to_ring (α : Type u) [self : comm_ring α] :
ring α
source
@[class]
structure comm_ring (α : Type u) :
Type u

A commutative ring is a ring with commutative multiplication.

Instances
source
@[instance]
def comm_ring.to_comm_monoid (α : Type u) [self : comm_ring α] :
comm_monoid α
source
@[instance]
def comm_ring.to_comm_semiring {α : Type u} [s : comm_ring α] :
comm_semiring α
Equations
source
theorem dvd_neg_of_dvd {α : Type u} [ring α] {a b : α} (h : a ∣ b) :
a ∣ -b
source
theorem dvd_of_dvd_neg {α : Type u} [ring α] {a b : α} (h : a ∣ -b) :
a ∣ b
source
@[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.

source
theorem neg_dvd_of_dvd {α : Type u} [ring α] {a b : α} (h : a ∣ b) :
-a ∣ b
source
theorem dvd_of_neg_dvd {α : Type u} [ring α] {a b : α} (h : -a ∣ b) :
a ∣ b
source
@[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.

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

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

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

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

source
theorem dvd_iff_dvd_of_dvd_sub {α : Type u} [ring α] {a b c : α} (h : a ∣ b - c) :
a ∣ b ↔ a ∣ c
source
@[simp]
theorem even_neg {α : Type u} [ring α] (a : α) :
even (-a) ↔ even a
source
theorem odd.neg {α : Type u} [ring α] {a : α} (hp : odd a) :
odd (-a)
source
@[simp]
theorem odd_neg {α : Type u} [ring α] (a : α) :
odd (-a) ↔ odd a
source
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) :
comm_ring β

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

Equations
source
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) :
comm_ring β

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

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

source
theorem mul_self_sub_one {α : Type u} [comm_ring α] (a : α) :
a * a - 1 = (a + 1) * (a - 1)
source
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.

source
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
source
theorem succ_ne_self {α : Type u} [ring α] [nontrivial α] (a : α) :
a + 1 ≠ a
source
theorem pred_ne_self {α : Type u} [ring α] [nontrivial α] (a : α) :
a - 1 ≠ a
source
theorem is_left_regular_of_non_zero_divisor {α : Type u} [ring α] (k : α) (h : ∀ (x : α), k * x = 0 → x = 0) :
is_left_regular k

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.

source
theorem is_right_regular_of_non_zero_divisor {α : Type u} [ring α] (k : α) (h : ∀ (x : α), x * k = 0 → x = 0) :
is_right_regular k

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.

source
theorem is_regular_of_ne_zero' {α : Type u} [ring α] [no_zero_divisors α] {k : α} (hk : k ≠ 0) :
is_regular k
source
@[instance]
def domain.to_ring (α : Type u) [self : domain α] :
ring α
source
@[class]
structure domain (α : 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 : α), domain.nsmul 0 x = 0) . "try_refl_tac"
  • nsmul_succ' : (∀ (n : ℕ) (x : α), domain.nsmul n.succ x = x + domain.nsmul n x) . "try_refl_tac"
  • neg : α → α
  • sub : α → α → α
  • sub_eq_add_neg : (∀ (a b : α), a - b = a + -b) . "try_refl_tac"
  • gsmul : ℤ → α → α
  • gsmul_zero' : (∀ (a : α), domain.gsmul 0 a = 0) . "try_refl_tac"
  • gsmul_succ' : (∀ (n : ℕ) (a : α), domain.gsmul (int.of_nat n.succ) a = a + domain.gsmul (int.of_nat n) a) . "try_refl_tac"
  • gsmul_neg' : (∀ (n : ℕ) (a : α), domain.gsmul -[1+ n] a = -domain.gsmul ↑(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 : α), domain.npow 0 x = 1) . "try_refl_tac"
  • npow_succ' : (∀ (n : ℕ) (x : α), domain.npow n.succ x = x * domain.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
  • exists_pair_ne : ∃ (x y : α), x ≠ y
  • eq_zero_or_eq_zero_of_mul_eq_zero : ∀ (a b : α), a * b = 0 → a = 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
source
@[instance]
def domain.to_nontrivial (α : Type u) [self : domain α] :
nontrivial α
source
@[instance]
def domain.to_no_zero_divisors {α : Type u} [domain α] :
no_zero_divisors α
source
@[instance]
def domain.to_cancel_monoid_with_zero {α : Type u} [domain α] :
cancel_monoid_with_zero α
Equations
source
def function.injective.domain {α : Type u} {β : Type v} [domain α] [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) :
domain β

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

Equations

Integral domains #

source
@[class]
structure integral_domain (α : Type u) :
Type u

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
source
@[instance]
def integral_domain.to_domain (α : Type u) [self : integral_domain α] :
domain α
source
@[instance]
def integral_domain.to_comm_ring (α : Type u) [self : integral_domain α] :
comm_ring α
source
@[instance]
def integral_domain.to_comm_cancel_monoid_with_zero {α : Type u} [integral_domain α] :
comm_cancel_monoid_with_zero α
Equations
source
def function.injective.integral_domain {α : Type u} {β : Type v} [integral_domain α] [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) :
integral_domain β

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

Equations
source
theorem mul_self_eq_mul_self_iff {α : Type u} [integral_domain α] {a b : α} :
a * a = b * b ↔ a = b ∨ a = -b
source
theorem mul_self_eq_one_iff {α : Type u} [integral_domain α] {a : α} :
a * a = 1 ↔ a = 1 ∨ a = -1
source
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.

source
def add_monoid_hom.mk_ring_hom_of_mul_self_of_two_ne_zero {α : Type u} {β : Type v} [integral_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
source
@[simp]
theorem add_monoid_hom.coe_fn_mk_ring_hom_of_mul_self_of_two_ne_zero {α : Type u} {β : Type v} [integral_domain α] [comm_ring β] (f : β →+ α) (h : ∀ (x : β), ⇑f (x * x) = (⇑f x) * ⇑f x) (h_two : 2 ≠ 0) (h_one : ⇑f 1 = 1) :
⇑(f.mk_ring_hom_of_mul_self_of_two_ne_zero h h_two h_one) = ⇑f
source
@[simp]
theorem add_monoid_hom.coe_add_monoid_hom_mk_ring_hom_of_mul_self_of_two_ne_zero {α : Type u} {β : Type v} [integral_domain α] [comm_ring β] (f : β →+ α) (h : ∀ (x : β), ⇑f (x * x) = (⇑f x) * ⇑f x) (h_two : 2 ≠ 0) (h_one : ⇑f 1 = 1) :
↑(f.mk_ring_hom_of_mul_self_of_two_ne_zero h h_two h_one) = f
source
def ring.inverse {M₀ : Type u_1} [monoid_with_zero M₀] :
M₀ → M₀

Introduce a function inverse on a monoid with zero M₀, 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.

Note that while this is in the ring namespace for brevity, it requires the weaker assumption monoid_with_zero M₀ instead of ring M₀.

Equations
source
@[simp]
theorem ring.inverse_unit {M₀ : Type u_1} [monoid_with_zero M₀] (u : units M₀) :
ring.inverse ↑u = ↑u⁻¹

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

source
@[simp]
theorem ring.inverse_non_unit {M₀ : Type u_1} [monoid_with_zero M₀] (x : M₀) (h : ¬is_unit x) :
ring.inverse x = 0

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

source
theorem ring.mul_inverse_cancel {M₀ : Type u_1} [monoid_with_zero M₀] (x : M₀) (h : is_unit x) :
x * ring.inverse x = 1
source
theorem ring.inverse_mul_cancel {M₀ : Type u_1} [monoid_with_zero M₀] (x : M₀) (h : is_unit x) :
(ring.inverse x) * x = 1
source
theorem ring.mul_inverse_cancel_right {M₀ : Type u_1} [monoid_with_zero M₀] (x y : M₀) (h : is_unit x) :
(y * x) * ring.inverse x = y
source
theorem ring.inverse_mul_cancel_right {M₀ : Type u_1} [monoid_with_zero M₀] (x y : M₀) (h : is_unit x) :
(y * ring.inverse x) * x = y
source
theorem ring.mul_inverse_cancel_left {M₀ : Type u_1} [monoid_with_zero M₀] (x y : M₀) (h : is_unit x) :
x * (ring.inverse x) * y = y
source
theorem ring.inverse_mul_cancel_left {M₀ : Type u_1} [monoid_with_zero M₀] (x y : M₀) (h : is_unit x) :
(ring.inverse x) * x * y = y
source
@[nolint]
def is_integral_domain.to_nontrivial {R : Type u} [ring R] (self : is_integral_domain R) :
nontrivial R
source
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 = 0 → x = 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.

source
theorem integral_domain.to_is_integral_domain (R : Type u) [integral_domain R] :
is_integral_domain R

Every integral domain satisfies the predicate for integral domains.

source
def is_integral_domain.to_integral_domain (R : Type u) [ring R] (h : is_integral_domain R) :
integral_domain R

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
source
@[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')
source
@[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
source
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)
source
@[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
source
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
source
@[simp]
theorem semiconj_by.neg_left_iff {R : Type x} [ring R] {a x y : R} :
semiconj_by (-a) x y ↔ semiconj_by a x y
source
@[simp]
theorem semiconj_by.neg_one_right {R : Type x} [ring R] (a : R) :
semiconj_by a (-1) (-1)
source
@[simp]
theorem semiconj_by.neg_one_left {R : Type x} [ring R] (x : R) :
semiconj_by (-1) x x
source
@[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')
source
@[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
source
@[simp]
theorem commute.add_right {R : Type x} [distrib R] {a b c : R} :
commute a b → commute a c → commute a (b + c)
source
@[simp]
theorem commute.add_left {R : Type x} [distrib R] {a b c : R} :
commute a c → commute b c → commute (a + b) c
source
theorem commute.bit0_right {R : Type x} [distrib R] {x y : R} (h : commute x y) :
commute x (bit0 y)
source
theorem commute.bit0_left {R : Type x} [distrib R] {x y : R} (h : commute x y) :
commute (bit0 x) y
source
theorem commute.bit1_right {R : Type x} [semiring R] {x y : R} (h : commute x y) :
commute x (bit1 y)
source
theorem commute.bit1_left {R : Type x} [semiring R] {x y : R} (h : commute x y) :
commute (bit1 x) y
source
theorem commute.neg_right {R : Type x} [ring R] {a b : R} :
commute a b → commute a (-b)
source
@[simp]
theorem commute.neg_right_iff {R : Type x} [ring R] {a b : R} :
commute a (-b) ↔ commute a b
source
theorem commute.neg_left {R : Type x} [ring R] {a b : R} :
commute a b → commute (-a) b
source
@[simp]
theorem commute.neg_left_iff {R : Type x} [ring R] {a b : R} :
commute (-a) b ↔ commute a b
source
@[simp]
theorem commute.neg_one_right {R : Type x} [ring R] (a : R) :
commute a (-1)
source
@[simp]
theorem commute.neg_one_left {R : Type x} [ring R] (a : R) :
commute (-1) a
source
@[simp]
theorem commute.sub_right {R : Type x} [ring R] {a b c : R} :
commute a b → commute a c → commute a (b - c)
source
@[simp]
theorem commute.sub_left {R : Type x} [ring R] {a b c : R} :
commute a c → commute b c → commute (a - b) c