algebra.ring.basic - mathlib docs

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.

Equations

function.injective.distrib f hf add mul = {mul := has_mul.mul _inst_1, add := has_add.add _inst_2, left_distrib := _, right_distrib := _}

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.

Equations

function.surjective.distrib f hf add mul = {mul := has_mul.mul _inst_3, add := has_add.add _inst_2, left_distrib := _, right_distrib := _}

source

@[instance]

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

add_comm_monoid α

source

@[instance]

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

distrib α

source

@[class]

structure semiring (α : Type u) :

Type 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
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 : α → α → α
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
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"
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

source

@[instance]

def semiring.to_monoid_with_zero (α : Type u) [s : semiring α] :

monoid_with_zero α

source

def function.injective.semiring {α : Type u} {β : Type v} [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) :

semiring β

Pullback a semiring instance along an injective function.

Equations

function.injective.semiring f hf zero one add mul = {add := add_comm_monoid.add (function.injective.add_comm_monoid f hf zero add), add_assoc := _, zero := monoid_with_zero.zero (function.injective.monoid_with_zero f hf zero one mul), zero_add := _, add_zero := _, nsmul := add_comm_monoid.nsmul (function.injective.add_comm_monoid f hf zero add), nsmul_zero' := _, nsmul_succ' := _, add_comm := _, mul := monoid_with_zero.mul (function.injective.monoid_with_zero f hf zero one mul), mul_assoc := _, one := monoid_with_zero.one (function.injective.monoid_with_zero f hf zero one mul), one_mul := _, mul_one := _, npow := monoid_with_zero.npow (function.injective.monoid_with_zero f hf zero one mul), npow_zero' := _, npow_succ' := _, zero_mul := _, mul_zero := _, left_distrib := _, right_distrib := _}

source

def function.surjective.semiring {α : Type u} {β : Type v} [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) :

semiring β

Pushforward a semiring instance along a surjective function.

Equations

function.surjective.semiring f hf zero one add mul = {add := add_comm_monoid.add (function.surjective.add_comm_monoid f hf zero add), add_assoc := _, zero := monoid_with_zero.zero (function.surjective.monoid_with_zero f hf zero one mul), zero_add := _, add_zero := _, nsmul := add_comm_monoid.nsmul (function.surjective.add_comm_monoid f hf zero add), nsmul_zero' := _, nsmul_succ' := _, add_comm := _, mul := monoid_with_zero.mul (function.surjective.monoid_with_zero f hf zero one mul), mul_assoc := _, one := monoid_with_zero.one (function.surjective.monoid_with_zero f hf zero one mul), one_mul := _, mul_one := _, npow := monoid_with_zero.npow (function.surjective.monoid_with_zero f hf zero one mul), npow_zero' := _, npow_succ' := _, zero_mul := _, mul_zero := _, left_distrib := _, right_distrib := _}

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

a * ite P 1 0 = ite P a 0

source

@[simp]

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

even a = ∃ (k : α), a = 2 * k

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_monoid_hom.mul_left {R : Type u_1} [semiring R] (r : R) :

R →+ R

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

Equations

add_monoid_hom.mul_left r = {to_fun := has_mul.mul r, map_zero' := _, map_add' := _}

source

@[simp]

theorem add_monoid_hom.coe_mul_left {R : Type u_1} [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} [semiring R] (r : R) :

R →+ R

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

Equations

add_monoid_hom.mul_right r = {to_fun := λ (a : R), a * r, map_zero' := _, map_add' := _}

source

@[simp]

theorem add_monoid_hom.coe_mul_right {R : Type u_1} [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} [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} [semiring α] [semiring β] (s : α →+* β) :

α →+ β

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

α →* β

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) [semiring α] [semiring β] :

Type (max u_1 u_2)

to_fun : α → β
map_one' : c.to_fun 1 = 1
map_mul' : ∀ (x y : α), c.to_fun (x * y) = (c.to_fun x) * c.to_fun y
map_zero' : c.to_fun 0 = 0
map_add' : ∀ (x y : α), c.to_fun (x + y) = c.to_fun x + c.to_fun y

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

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

source

@[instance]

def ring_hom.has_coe_to_fun {α : Type u} {β : Type v} {rα : semiring α} {rβ : semiring β} :

has_coe_to_fun (α →+* β)

Equations

ring_hom.has_coe_to_fun = {F := λ (x : α →+* β), α → β, coe := ring_hom.to_fun rβ}

source

@[simp]

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

f.to_fun = ⇑f

source

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

source

@[instance]

def ring_hom.has_coe_monoid_hom {α : Type u} {β : Type v} {rα : semiring α} {rβ : semiring β} :

has_coe (α →+* β) (α →* β)

Equations

ring_hom.has_coe_monoid_hom = {coe := ring_hom.to_monoid_hom rβ}

source

@[simp]

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

⇑↑f = ⇑f

source

@[simp]

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

f.to_monoid_hom = ↑f

source

@[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₂}

source

@[instance]

def ring_hom.has_coe_add_monoid_hom {α : Type u} {β : Type v} {rα : semiring α} {rβ : semiring β} :

has_coe (α →+* β) (α →+ β)

Equations

ring_hom.has_coe_add_monoid_hom = {coe := ring_hom.to_add_monoid_hom rβ}

source

@[simp]

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

⇑↑f = ⇑f

source

@[simp]

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

f.to_add_monoid_hom = ↑f

source

@[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₄}

source

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

⇑f x = ⇑g x

source

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

⇑f x = ⇑f y

source

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

f = g

source

@[ext]

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

f = g

source

theorem ring_hom.ext_iff {α : Type u} {β : Type v} {rα : semiring α} {rβ : semiring β} {f g : α →+* β} :

f = g ↔ ∀ (x : α), ⇑f x = ⇑g x

source

@[simp]

theorem ring_hom.mk_coe {α : 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

source

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

function.injective coe

source

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

function.injective coe

source

@[simp]

theorem ring_hom.map_zero {α : Type u} {β : Type v} {rα : semiring α} {rβ : semiring β} (f : α →+* β) :

⇑f 0 = 0

Ring homomorphisms map zero to zero.

source

@[simp]

theorem ring_hom.map_one {α : Type u} {β : Type v} {rα : semiring α} {rβ : semiring β} (f : α →+* β) :

⇑f 1 = 1

Ring homomorphisms map one to one.

source

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

source

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

source

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

source

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

source

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.

source

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.

source

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

source

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

source

theorem ring_hom.domain_nontrivial {α : Type u} {β : Type v} {rα : semiring α} {rβ : 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} {rα : semiring α} {rβ : semiring β} (f : α →+* β) {a : α} (h : is_unit a) :

is_unit (⇑f a)

source

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

α →+* α

The identity ring homomorphism from a semiring to itself.

Equations

ring_hom.id α = {to_fun := id α, map_one' := _, map_mul' := _, map_zero' := _, map_add' := _}

source

@[instance]

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

inhabited (α →+* α)

Equations

ring_hom.inhabited = {default := ring_hom.id α rα}

source

@[simp]

theorem ring_hom.id_apply {α : Type u} [rα : semiring α] (x : α) :

⇑(ring_hom.id α) x = x

source

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

α →+* γ

Composition of ring homomorphisms is a ring homomorphism.

Equations

hnp.comp hmn = {to_fun := ⇑hnp ∘ ⇑hmn, map_one' := _, map_mul' := _, map_zero' := _, map_add' := _}

source

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.

source

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

source

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)

source

@[simp]

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

f.comp (ring_hom.id α) = f

source

@[simp]

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

(ring_hom.id β).comp f = f

source

@[instance]

def ring_hom.monoid {α : Type u} [rα : semiring α] :

monoid (α →+* α)

Equations

ring_hom.monoid = {mul := ring_hom.comp rα, mul_assoc := _, one := ring_hom.id α rα, one_mul := _, mul_one := _, npow := npow_rec (mul_one_class.to_has_mul (α →+* α)), npow_zero' := _, npow_succ' := _}

source

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

1 = ring_hom.id α

source

@[simp]

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

⇑1 = id

source

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

f * g = f.comp g

source

@[simp]

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

⇑f * g = ⇑f ∘ ⇑g

source

theorem ring_hom.cancel_right {α : Type u} {β : Type v} {γ : Type w} [rα : semiring α] [rβ : semiring β] {rγ : 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α : semiring α] [rβ : semiring β] {rγ : semiring γ} {g : β →+* γ} {f₁ f₂ : α →+* β} (hg : function.injective ⇑g) :

g.comp f₁ = g.comp f₂ ↔ f₁ = f₂

source

@[class]

structure comm_semiring (α : Type u) :

Type 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
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 : α → α → α
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
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"
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

source

@[instance]

def comm_semiring.to_comm_monoid (α : Type u) [s : comm_semiring α] :

comm_monoid α

source

@[instance]

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

semiring α

source

@[instance]

def comm_semiring.to_comm_monoid_with_zero {α : Type u} [comm_semiring α] :

comm_monoid_with_zero α

Equations

comm_semiring.to_comm_monoid_with_zero = {mul := comm_monoid.mul (comm_semiring.to_comm_monoid α), mul_assoc := _, one := comm_monoid.one (comm_semiring.to_comm_monoid α), one_mul := _, mul_one := _, npow := comm_monoid.npow (comm_semiring.to_comm_monoid α), npow_zero' := _, npow_succ' := _, mul_comm := _, zero := semiring.zero (comm_semiring.to_semiring α), zero_mul := _, mul_zero := _}

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.

Equations

function.injective.comm_semiring f hf zero one add mul = {add := semiring.add (function.injective.semiring f hf zero one add mul), add_assoc := _, zero := semiring.zero (function.injective.semiring f hf zero one add mul), zero_add := _, add_zero := _, nsmul := semiring.nsmul (function.injective.semiring f hf zero one add mul), nsmul_zero' := _, nsmul_succ' := _, add_comm := _, mul := semiring.mul (function.injective.semiring f hf zero one add mul), mul_assoc := _, one := semiring.one (function.injective.semiring f hf zero one add mul), one_mul := _, mul_one := _, npow := semiring.npow (function.injective.semiring f hf zero one add mul), npow_zero' := _, npow_succ' := _, zero_mul := _, mul_zero := _, left_distrib := _, right_distrib := _, mul_comm := _}

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.

Equations

function.surjective.comm_semiring f hf zero one add mul = {add := semiring.add (function.surjective.semiring f hf zero one add mul), add_assoc := _, zero := semiring.zero (function.surjective.semiring f hf zero one add mul), zero_add := _, add_zero := _, nsmul := semiring.nsmul (function.surjective.semiring f hf zero one add mul), nsmul_zero' := _, nsmul_succ' := _, add_comm := _, mul := semiring.mul (function.surjective.semiring f hf zero one add mul), mul_assoc := _, one := semiring.one (function.surjective.semiring f hf zero one add mul), one_mul := _, mul_one := _, npow := semiring.npow (function.surjective.semiring f hf zero one add mul), npow_zero' := _, npow_succ' := _, zero_mul := _, mul_zero := _, left_distrib := _, right_distrib := _, mul_comm := _}

source

theorem add_mul_self_eq {α : Type u} [comm_semiring α] (a b : α) :

(a + b) * (a + b) = a * a + (2 * a) * b + b * b

source

@[simp]

theorem two_dvd_bit0 {α : Type u} [comm_semiring α] {a : α} :

2 ∣ bit0 a

source

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

a ∣ b → ⇑f a ∣ ⇑f b

source

@[instance]

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

add_comm_group α

source

@[instance]

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

monoid α

source

@[class]

structure ring (α : Type u) :

Type 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
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"
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
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_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

source

@[instance]

def ring.to_distrib (α : Type u) [s : ring α] :

distrib α

source

@[instance]

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

semiring α

Equations

ring.to_semiring = {add := ring.add _inst_1, add_assoc := _, zero := ring.zero _inst_1, zero_add := _, add_zero := _, nsmul := ring.nsmul _inst_1, nsmul_zero' := _, nsmul_succ' := _, add_comm := _, mul := ring.mul _inst_1, mul_assoc := _, one := ring.one _inst_1, one_mul := _, mul_one := _, npow := ring.npow _inst_1, npow_zero' := _, npow_succ' := _, zero_mul := _, mul_zero := _, left_distrib := _, right_distrib := _}

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.

Equations

function.injective.ring f hf zero one add mul neg sub = {add := add_comm_group.add (function.injective.add_comm_group f hf zero add neg sub), add_assoc := _, zero := add_comm_group.zero (function.injective.add_comm_group f hf zero add neg sub), zero_add := _, add_zero := _, nsmul := add_comm_group.nsmul (function.injective.add_comm_group f hf zero add neg sub), nsmul_zero' := _, nsmul_succ' := _, neg := add_comm_group.neg (function.injective.add_comm_group f hf zero add neg sub), sub := add_comm_group.sub (function.injective.add_comm_group f hf zero add neg sub), sub_eq_add_neg := _, add_left_neg := _, add_comm := _, mul := monoid.mul (function.injective.monoid f hf one mul), mul_assoc := _, one := monoid.one (function.injective.monoid f hf one mul), one_mul := _, mul_one := _, npow := npow (function.injective.monoid f hf one mul), npow_zero' := _, npow_succ' := _, left_distrib := _, right_distrib := _}

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.

Equations

function.surjective.ring f hf zero one add mul neg sub = {add := add_comm_group.add (function.surjective.add_comm_group f hf zero add neg sub), add_assoc := _, zero := add_comm_group.zero (function.surjective.add_comm_group f hf zero add neg sub), zero_add := _, add_zero := _, nsmul := add_comm_group.nsmul (function.surjective.add_comm_group f hf zero add neg sub), nsmul_zero' := _, nsmul_succ' := _, neg := add_comm_group.neg (function.surjective.add_comm_group f hf zero add neg sub), sub := add_comm_group.sub (function.surjective.add_comm_group f hf zero add neg sub), sub_eq_add_neg := _, add_left_neg := _, add_comm := _, mul := monoid.mul (function.surjective.monoid f hf one mul), mul_assoc := _, one := monoid.one (function.surjective.monoid f hf one mul), one_mul := _, mul_one := _, npow := npow (function.surjective.monoid f hf one mul), npow_zero' := _, npow_succ' := _, left_distrib := _, right_distrib := _}

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

units.has_neg = {neg := λ (u : units α), {val := -↑u, inv := -↑u⁻¹, val_inv := _, inv_val := _}}

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 α] [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} [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

ring_hom.mk' f map_add = {to_fun := ⇑f, map_one' := _, map_mul' := _, map_zero' := _, map_add' := _}

source

@[instance]

def comm_ring.to_ring (α : Type u) [s : comm_ring α] :

ring α

source

@[class]

structure comm_ring (α : Type u) :

Type 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
nsmul : ℕ → α → α
nsmul_zero' : (∀ (x : α), comm_ring.nsmul 0 x = 0) . "try_refl_tac"
nsmul_succ' : (∀ (n : ℕ) (x : α), comm_ring.nsmul n.succ x = x + comm_ring.nsmul n x) . "try_refl_tac"
neg : α → α
sub : α → α → α
sub_eq_add_neg : (∀ (a b : α), a - b = a + -b) . "try_refl_tac"
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
npow : ℕ → α → α
npow_zero' : (∀ (x : α), comm_ring.npow 0 x = 1) . "try_refl_tac"
npow_succ' : (∀ (n : ℕ) (x : α), comm_ring.npow n.succ x = x * comm_ring.npow n x) . "try_refl_tac"
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

source

@[instance]

def comm_ring.to_comm_monoid (α : Type u) [s : comm_ring α] :

comm_monoid α

source

@[instance]

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

comm_semiring α

Equations

comm_ring.to_comm_semiring = {add := comm_ring.add s, add_assoc := _, zero := comm_ring.zero s, zero_add := _, add_zero := _, nsmul := comm_ring.nsmul s, nsmul_zero' := _, nsmul_succ' := _, add_comm := _, mul := comm_ring.mul s, mul_assoc := _, one := comm_ring.one s, one_mul := _, mul_one := _, npow := comm_ring.npow s, npow_zero' := _, npow_succ' := _, zero_mul := _, mul_zero := _, left_distrib := _, right_distrib := _, mul_comm := _}

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.

Equations

function.injective.comm_ring f hf zero one add mul neg sub = {add := ring.add (function.injective.ring f hf zero one add mul neg sub), add_assoc := _, zero := ring.zero (function.injective.ring f hf zero one add mul neg sub), zero_add := _, add_zero := _, nsmul := ring.nsmul (function.injective.ring f hf zero one add mul neg sub), nsmul_zero' := _, nsmul_succ' := _, neg := ring.neg (function.injective.ring f hf zero one add mul neg sub), sub := ring.sub (function.injective.ring f hf zero one add mul neg sub), sub_eq_add_neg := _, add_left_neg := _, add_comm := _, mul := ring.mul (function.injective.ring f hf zero one add mul neg sub), mul_assoc := _, one := ring.one (function.injective.ring f hf zero one add mul neg sub), one_mul := _, mul_one := _, npow := ring.npow (function.injective.ring f hf zero one add mul neg sub), npow_zero' := _, npow_succ' := _, left_distrib := _, right_distrib := _, mul_comm := _}

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.

Equations

function.surjective.comm_ring f hf zero one add mul neg sub = {add := ring.add (function.surjective.ring f hf zero one add mul neg sub), add_assoc := _, zero := ring.zero (function.surjective.ring f hf zero one add mul neg sub), zero_add := _, add_zero := _, nsmul := ring.nsmul (function.surjective.ring f hf zero one add mul neg sub), nsmul_zero' := _, nsmul_succ' := _, neg := ring.neg (function.surjective.ring f hf zero one add mul neg sub), sub := ring.sub (function.surjective.ring f hf zero one add mul neg sub), sub_eq_add_neg := _, add_left_neg := _, add_comm := _, mul := ring.mul (function.surjective.ring f hf zero one add mul neg sub), mul_assoc := _, one := ring.one (function.surjective.ring f hf zero one add mul neg sub), one_mul := _, mul_one := _, npow := ring.npow (function.surjective.ring f hf zero one add mul neg sub), npow_zero' := _, npow_succ' := _, left_distrib := _, right_distrib := _, mul_comm := _}

source

theorem dvd_neg_of_dvd {α : Type u} [comm_ring α] {a b : α} (h : a ∣ b) :

a ∣ -b

source

theorem dvd_of_dvd_neg {α : Type u} [comm_ring α] {a b : α} (h : a ∣ -b) :

a ∣ b

source

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

a ∣ -b ↔ a ∣ b

source

theorem neg_dvd_of_dvd {α : Type u} [comm_ring α] {a b : α} (h : a ∣ b) :

-a ∣ b

source

theorem dvd_of_neg_dvd {α : Type u} [comm_ring α] {a b : α} (h : -a ∣ b) :

a ∣ b

source

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

-a ∣ b ↔ a ∣ b

source

theorem dvd_sub {α : Type u} [comm_ring α] {a b c : α} (h₁ : a ∣ b) (h₂ : a ∣ c) :

a ∣ b - c

source

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

a ∣ b ↔ a ∣ b + c

source

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

a ∣ c ↔ a ∣ b + c

source

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

2 ∣ bit1 a ↔ 2 ∣ 1

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

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

source

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

source

theorem dvd_add_left {α : Type u} [comm_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} [comm_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} [comm_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} [comm_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 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 dvd_iff_dvd_of_dvd_sub {α : Type u} [comm_ring α] {a b c : α} (h : a ∣ b - c) :

a ∣ b ↔ a ∣ c

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

@[instance]

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

ring α

source

@[class]

structure domain (α : Type u) :

Type 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
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"
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
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_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 = 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) [s : 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

domain.to_cancel_monoid_with_zero = {mul := semiring.mul infer_instance, mul_assoc := _, one := semiring.one infer_instance, one_mul := _, mul_one := _, npow := semiring.npow infer_instance, npow_zero' := _, npow_succ' := _, zero := semiring.zero infer_instance, zero_mul := _, mul_zero := _, mul_left_cancel_of_ne_zero := _, mul_right_cancel_of_ne_zero := _}

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.

Equations

function.injective.domain f hf zero one add mul neg sub = {add := ring.add (function.injective.ring f hf zero one add mul neg sub), add_assoc := _, zero := ring.zero (function.injective.ring f hf zero one add mul neg sub), zero_add := _, add_zero := _, nsmul := ring.nsmul (function.injective.ring f hf zero one add mul neg sub), nsmul_zero' := _, nsmul_succ' := _, neg := ring.neg (function.injective.ring f hf zero one add mul neg sub), sub := ring.sub (function.injective.ring f hf zero one add mul neg sub), sub_eq_add_neg := _, add_left_neg := _, add_comm := _, mul := ring.mul (function.injective.ring f hf zero one add mul neg sub), mul_assoc := _, one := ring.one (function.injective.ring f hf zero one add mul neg sub), one_mul := _, mul_one := _, npow := ring.npow (function.injective.ring f hf zero one add mul neg sub), npow_zero' := _, npow_succ' := _, left_distrib := _, right_distrib := _, exists_pair_ne := _, eq_zero_or_eq_zero_of_mul_eq_zero := _}

source

@[class]

structure integral_domain (α : Type u) :

Type 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
nsmul : ℕ → α → α
nsmul_zero' : (∀ (x : α), integral_domain.nsmul 0 x = 0) . "try_refl_tac"
nsmul_succ' : (∀ (n : ℕ) (x : α), integral_domain.nsmul n.succ x = x + integral_domain.nsmul n x) . "try_refl_tac"
neg : α → α
sub : α → α → α
sub_eq_add_neg : (∀ (a b : α), a - b = a + -b) . "try_refl_tac"
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
npow : ℕ → α → α
npow_zero' : (∀ (x : α), integral_domain.npow 0 x = 1) . "try_refl_tac"
npow_succ' : (∀ (n : ℕ) (x : α), integral_domain.npow n.succ x = x * integral_domain.npow n x) . "try_refl_tac"
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 = 0 → a = 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

source

@[instance]

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

domain α

source

@[instance]

def integral_domain.to_comm_ring (α : Type u) [s : 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.

Equations

function.injective.integral_domain f hf zero one add mul neg sub = {add := comm_ring.add (function.injective.comm_ring f hf zero one add mul neg sub), add_assoc := _, zero := comm_ring.zero (function.injective.comm_ring f hf zero one add mul neg sub), zero_add := _, add_zero := _, nsmul := comm_ring.nsmul (function.injective.comm_ring f hf zero one add mul neg sub), nsmul_zero' := _, nsmul_succ' := _, neg := comm_ring.neg (function.injective.comm_ring f hf zero one add mul neg sub), sub := comm_ring.sub (function.injective.comm_ring f hf zero one add mul neg sub), sub_eq_add_neg := _, add_left_neg := _, add_comm := _, mul := comm_ring.mul (function.injective.comm_ring f hf zero one add mul neg sub), mul_assoc := _, one := comm_ring.one (function.injective.comm_ring f hf zero one add mul neg sub), one_mul := _, mul_one := _, npow := comm_ring.npow (function.injective.comm_ring f hf zero one add mul neg sub), npow_zero' := _, npow_succ' := _, left_distrib := _, right_distrib := _, mul_comm := _, exists_pair_ne := _, eq_zero_or_eq_zero_of_mul_eq_zero := _}

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

f.mk_ring_hom_of_mul_self_of_two_ne_zero h h_two h_one = {to_fun := f.to_fun, map_one' := h_one, map_mul' := _, map_zero' := _, map_add' := _}

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

ring.inverse = λ (x : M₀), dite (is_unit x) (λ (h : is_unit x), ↑(classical.some h)⁻¹) (λ (h : ¬is_unit x), 0)

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

@[nolint]

def is_integral_domain.to_nontrivial {R : Type u} [ring R] (s : 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