mathlib docs: algebra.ring.basic

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

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

⇑f = ⇑g → f = g

source

@[ext]

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

(∀ (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

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

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

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

@[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 γ} :

(β →+* γ) → (α →+* β) → α →+* γ

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 := _}

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 : α →+* β} :

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₂ : α →+* β} :

function.injective ⇑g → (g.comp f₁ = g.comp f₂ ↔ f₁ = f₂)

source

@[instance]

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

semiring α

source

@[instance]

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

comm_monoid α

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
add_comm : ∀ (a b : α), a + b = b + a
mul : α → α → α
mul_assoc : ∀ (a b c_1 : α), a * b * c_1 = a * (b * c_1)
one : α
one_mul : ∀ (a : α), 1 * a = a
mul_one : ∀ (a : α), a * 1 = a
zero_mul : ∀ (a : α), 0 * a = 0
mul_zero : ∀ (a : α), a * 0 = 0
left_distrib : ∀ (a b c_1 : α), a * (b + c_1) = a * b + a * c_1
right_distrib : ∀ (a b c_1 : α), (a + b) * c_1 = a * c_1 + b * c_1
mul_comm : ∀ (a b : α), a * b = b * a

Instances

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 := _, mul_comm := _, zero := semiring.zero (comm_semiring.to_semiring α), zero_mul := _, mul_zero := _}

source

@[instance]

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

comm_monoid_with_zero α

Equations

comm_semiring.comm_monoid_with_zero = {mul := comm_semiring.mul _inst_1, mul_assoc := _, one := comm_semiring.one _inst_1, one_mul := _, mul_one := _, mul_comm := _, zero := comm_semiring.zero _inst_1, 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 : γ → α) :

function.injective f → f 0 = 0 → f 1 = 1 → (∀ (x y : γ), f (x + y) = f x + f y) → (∀ (x y : γ), f (x * y) = f x * f y) → comm_semiring γ

Pullback a semiring instance along an injective function.

Equations

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 := _, 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 := _, 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 : α → γ) :

function.surjective f → f 0 = 0 → f 1 = 1 → (∀ (x y : α), f (x + y) = f x + f y) → (∀ (x y : α), f (x * y) = f x * f y) → comm_semiring γ

Pullback a semiring instance along an injective function.

Equations

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 := _, 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 := _, 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

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

a ∣ b → a ∣ c → a ∣ b + c

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_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
neg : α → α
add_left_neg : ∀ (a : α), -a + a = 0
add_comm : ∀ (a b : α), a + b = b + a
mul : α → α → α
mul_assoc : ∀ (a b c_1 : α), a * b * c_1 = a * (b * c_1)
one : α
one_mul : ∀ (a : α), 1 * a = a
mul_one : ∀ (a : α), a * 1 = a
left_distrib : ∀ (a b c_1 : α), a * (b + c_1) = a * b + a * c_1
right_distrib : ∀ (a b c_1 : α), (a + b) * c_1 = a * c_1 + b * c_1

Instances

source

@[instance]

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

distrib α

source

@[instance]

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

add_comm_group α

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 := _, add_comm := _, mul := ring.mul _inst_1, mul_assoc := _, one := ring.one _inst_1, one_mul := _, mul_one := _, 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 β] (f : β → α) :

function.injective f → f 0 = 0 → f 1 = 1 → (∀ (x y : β), f (x + y) = f x + f y) → (∀ (x y : β), f (x * y) = f x * f y) → (∀ (x : β), f (-x) = -f x) → ring β

Pullback a ring instance along an injective function.

Equations

function.injective.ring f hf zero one add mul neg = {add := add_comm_group.add (function.injective.add_comm_group f hf zero add neg), add_assoc := _, zero := add_comm_group.zero (function.injective.add_comm_group f hf zero add neg), zero_add := _, add_zero := _, neg := add_comm_group.neg (function.injective.add_comm_group f hf zero 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 := _, left_distrib := _, right_distrib := _}

source

def function.surjective.ring {α : Type u} {β : Type v} [ring α] [has_zero β] [has_one β] [has_add β] [has_mul β] [has_neg β] (f : α → β) :

function.surjective f → f 0 = 0 → f 1 = 1 → (∀ (x y : α), f (x + y) = f x + f y) → (∀ (x y : α), f (x * y) = f x * f y) → (∀ (x : α), f (-x) = -f x) → ring β

Pullback a ring instance along an injective function.

Equations

function.surjective.ring f hf zero one add mul neg = {add := add_comm_group.add (function.surjective.add_comm_group f hf zero add neg), add_assoc := _, zero := add_comm_group.zero (function.surjective.add_comm_group f hf zero add neg), zero_add := _, add_zero := _, neg := add_comm_group.neg (function.surjective.add_comm_group f hf zero 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 := _, 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_right_distrib {α : Type u} [ring α] (a b c : α) :

(a - b) * c = a * c - b * c

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

@[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 : α →* γ) :

(∀ (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

@[instance]

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

comm_semigroup α

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
neg : α → α
add_left_neg : ∀ (a : α), -a + a = 0
add_comm : ∀ (a b : α), a + b = b + a
mul : α → α → α
mul_assoc : ∀ (a b c_1 : α), a * b * c_1 = a * (b * c_1)
one : α
one_mul : ∀ (a : α), 1 * a = a
mul_one : ∀ (a : α), a * 1 = a
left_distrib : ∀ (a b c_1 : α), a * (b + c_1) = a * b + a * c_1
right_distrib : ∀ (a b c_1 : α), (a + b) * c_1 = a * c_1 + b * c_1
mul_comm : ∀ (a b : α), a * b = b * a

Instances

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 := _, add_comm := _, mul := comm_ring.mul s, mul_assoc := _, one := comm_ring.one s, one_mul := _, mul_one := _, 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 β] (f : β → α) :

function.injective f → f 0 = 0 → f 1 = 1 → (∀ (x y : β), f (x + y) = f x + f y) → (∀ (x y : β), f (x * y) = f x * f y) → (∀ (x : β), f (-x) = -f x) → comm_ring β

Pullback a ring instance along an injective function.

Equations

function.injective.comm_ring f hf zero one add mul neg = {add := ring.add (function.injective.ring f hf zero one add mul neg), add_assoc := _, zero := ring.zero (function.injective.ring f hf zero one add mul neg), zero_add := _, add_zero := _, neg := ring.neg (function.injective.ring f hf zero one add mul neg), add_left_neg := _, add_comm := _, mul := ring.mul (function.injective.ring f hf zero one add mul neg), mul_assoc := _, one := ring.one (function.injective.ring f hf zero one add mul neg), one_mul := _, mul_one := _, 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 β] (f : α → β) :

function.surjective f → f 0 = 0 → f 1 = 1 → (∀ (x y : α), f (x + y) = f x + f y) → (∀ (x y : α), f (x * y) = f x * f y) → (∀ (x : α), f (-x) = -f x) → comm_ring β

Pullback a ring instance along an injective function.

Equations

function.surjective.comm_ring f hf zero one add mul neg = {add := ring.add (function.surjective.ring f hf zero one add mul neg), add_assoc := _, zero := ring.zero (function.surjective.ring f hf zero one add mul neg), zero_add := _, add_zero := _, neg := ring.neg (function.surjective.ring f hf zero one add mul neg), add_left_neg := _, add_comm := _, mul := ring.mul (function.surjective.ring f hf zero one add mul neg), mul_assoc := _, one := ring.one (function.surjective.ring f hf zero one add mul neg), one_mul := _, mul_one := _, left_distrib := _, right_distrib := _, mul_comm := _}

source

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

a * a - b * b = (a + b) * (a - b)

source

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

a * a - 1 = (a + 1) * (a - 1)

source

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

a ∣ b → a ∣ -b

source

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

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 : α} :

a ∣ b → -a ∣ b

source

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

-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 : α} :

a ∣ b → a ∣ c → a ∣ b - c

source

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

a ∣ c → (a ∣ b ↔ a ∣ b + c)

source

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

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

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

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 : α} :

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 : α} :

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 : α} :

k ∣ a - b → k ∣ x - y → k ∣ a * x - b * y

source

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

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

nontrivial α

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
neg : α → α
add_left_neg : ∀ (a : α), -a + a = 0
add_comm : ∀ (a b : α), a + b = b + a
mul : α → α → α
mul_assoc : ∀ (a b c_1 : α), a * b * c_1 = a * (b * c_1)
one : α
one_mul : ∀ (a : α), 1 * a = a
mul_one : ∀ (a : α), a * 1 = a
left_distrib : ∀ (a b c_1 : α), a * (b + c_1) = a * b + a * c_1
right_distrib : ∀ (a b c_1 : α), (a + b) * c_1 = a * c_1 + b * c_1
exists_pair_ne : ∃ (x y : α), x ≠ y
eq_zero_or_eq_zero_of_mul_eq_zero : ∀ (a b : α), a * b = 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_no_zero_divisors {α : Type u} [domain α] :

no_zero_divisors α

Equations

domain.to_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 := _, 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 β] (f : β → α) :

function.injective f → f 0 = 0 → f 1 = 1 → (∀ (x y : β), f (x + y) = f x + f y) → (∀ (x y : β), f (x * y) = f x * f y) → (∀ (x : β), f (-x) = -f x) → domain β

Pullback a domain instance along an injective function.

Equations

function.injective.domain f hf zero one add mul neg = {add := ring.add (function.injective.ring f hf zero one add mul neg), add_assoc := _, zero := ring.zero (function.injective.ring f hf zero one add mul neg), zero_add := _, add_zero := _, neg := ring.neg (function.injective.ring f hf zero one add mul neg), add_left_neg := _, add_comm := _, mul := ring.mul (function.injective.ring f hf zero one add mul neg), mul_assoc := _, one := ring.one (function.injective.ring f hf zero one add mul neg), one_mul := _, mul_one := _, left_distrib := _, right_distrib := _, exists_pair_ne := _, eq_zero_or_eq_zero_of_mul_eq_zero := _}

source

@[instance]

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

comm_ring α

source

@[instance]

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

domain α

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
neg : α → α
add_left_neg : ∀ (a : α), -a + a = 0
add_comm : ∀ (a b : α), a + b = b + a
mul : α → α → α
mul_assoc : ∀ (a b c_1 : α), a * b * c_1 = a * (b * c_1)
one : α
one_mul : ∀ (a : α), 1 * a = a
mul_one : ∀ (a : α), a * 1 = a
left_distrib : ∀ (a b c_1 : α), a * (b + c_1) = a * b + a * c_1
right_distrib : ∀ (a b c_1 : α), (a + b) * c_1 = a * c_1 + b * c_1
mul_comm : ∀ (a b : α), a * b = b * a
exists_pair_ne : ∃ (x y : α), x ≠ y
eq_zero_or_eq_zero_of_mul_eq_zero : ∀ (a b : α), a * b = 0 → a = 0 ∨ b = 0

Instances

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 β] (f : β → α) :

function.injective f → f 0 = 0 → f 1 = 1 → (∀ (x y : β), f (x + y) = f x + f y) → (∀ (x y : β), f (x * y) = f x * f y) → (∀ (x : β), f (-x) = -f x) → integral_domain β

Pullback an integral_domain instance along an injective function.

Equations

function.injective.integral_domain f hf zero one add mul neg = {add := comm_ring.add (function.injective.comm_ring f hf zero one add mul neg), add_assoc := _, zero := comm_ring.zero (function.injective.comm_ring f hf zero one add mul neg), zero_add := _, add_zero := _, neg := comm_ring.neg (function.injective.comm_ring f hf zero one add mul neg), add_left_neg := _, add_comm := _, mul := comm_ring.mul (function.injective.comm_ring f hf zero one add mul neg), mul_assoc := _, one := comm_ring.one (function.injective.comm_ring f hf zero one add mul neg), one_mul := _, mul_one := _, 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 ring.inverse {R : Type x} [ring R] :

R → R

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

Equations

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

source

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

ring.inverse ↑a = ↑a⁻¹

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

source

@[nolint]

def is_integral_domain.to_nontrivial {R : Type u} [ring R] :

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

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