mathlib docs: algebra.field

source

@[instance]

def division_ring.to_nontrivial (α : Type u) [s : division_ring α] :

nontrivial α

source

@[instance]

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

ring α

source

@[class]

structure division_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
inv : α → α
exists_pair_ne : ∃ (x y : α), x ≠ y
mul_inv_cancel : ∀ {a : α}, a ≠ 0 → a * a⁻¹ = 1
inv_mul_cancel : ∀ {a : α}, a ≠ 0 → a⁻¹ * a = 1
inv_zero : 0⁻¹ = 0

A division_ring is a ring with multiplicative inverses for nonzero elements

Instances

source

@[instance]

def division_ring.to_has_inv (α : Type u) [s : division_ring α] :

has_inv α

source

@[instance]

def division_ring_has_div {α : Type u} [division_ring α] :

has_div α

Equations

division_ring_has_div = {div := λ (a b : α), a * b⁻¹}

source

@[instance]

def division_ring.to_group_with_zero {α : Type u} [division_ring α] :

group_with_zero α

Every division ring is a group_with_zero.

Equations

division_ring.to_group_with_zero = {mul := division_ring.mul _inst_1, mul_assoc := _, one := division_ring.one _inst_1, one_mul := _, mul_one := _, zero := division_ring.zero _inst_1, zero_mul := _, mul_zero := _, inv := division_ring.inv _inst_1, exists_pair_ne := _, inv_zero := _, mul_inv_cancel := _}

source

theorem inv_eq_one_div {α : Type u} [division_ring α] (a : α) :

a⁻¹ = 1 / a

source

theorem mul_div_assoc' {α : Type u} [division_ring α] (a b c : α) :

a * (b / c) = a * b / c

source

theorem one_div_neg_one_eq_neg_one {α : Type u} [division_ring α] :

1 / -1 = -1

source

theorem one_div_neg_eq_neg_one_div {α : Type u} [division_ring α] (a : α) :

1 / -a = -(1 / a)

source

theorem div_neg_eq_neg_div {α : Type u} [division_ring α] (a b : α) :

b / -a = -(b / a)

source

theorem neg_div {α : Type u} [division_ring α] (a b : α) :

-b / a = -(b / a)

source

theorem neg_div' {α : Type u_1} [division_ring α] (a b : α) :

-(b / a) = -b / a

source

theorem neg_div_neg_eq {α : Type u} [division_ring α] (a b : α) :

-a / -b = a / b

source

theorem div_add_div_same {α : Type u} [division_ring α] (a b c : α) :

a / c + b / c = (a + b) / c

source

theorem div_sub_div_same {α : Type u} [division_ring α] (a b c : α) :

a / c - b / c = (a - b) / c

source

theorem neg_inv {α : Type u} [division_ring α] {a : α} :

-a⁻¹ = (-a)⁻¹

source

theorem add_div {α : Type u} [division_ring α] (a b c : α) :

(a + b) / c = a / c + b / c

source

theorem sub_div {α : Type u} [division_ring α] (a b c : α) :

(a - b) / c = a / c - b / c

source

theorem div_neg {α : Type u} [division_ring α] {b : α} (a : α) :

a / -b = -(a / b)

source

theorem inv_neg {α : Type u} [division_ring α] {a : α} :

(-a)⁻¹ = -a⁻¹

source

theorem one_div_mul_add_mul_one_div_eq_one_div_add_one_div {α : Type u} [division_ring α] {a b : α} :

a ≠ 0 → b ≠ 0 → 1 / a * (a + b) * (1 / b) = 1 / a + 1 / b

source

theorem one_div_mul_sub_mul_one_div_eq_one_div_add_one_div {α : Type u} [division_ring α] {a b : α} :

a ≠ 0 → b ≠ 0 → 1 / a * (b - a) * (1 / b) = 1 / a - 1 / b

source

theorem add_div_eq_mul_add_div {α : Type u} [division_ring α] (a b : α) {c : α} :

c ≠ 0 → a + b / c = (a * c + b) / c

source

@[instance]

def division_ring.to_domain {α : Type u} [division_ring α] :

domain α

Equations

division_ring.to_domain = {add := division_ring.add _inst_1, add_assoc := _, zero := division_ring.zero _inst_1, zero_add := _, add_zero := _, neg := division_ring.neg _inst_1, add_left_neg := _, add_comm := _, mul := division_ring.mul _inst_1, mul_assoc := _, one := division_ring.one _inst_1, one_mul := _, mul_one := _, left_distrib := _, right_distrib := _, exists_pair_ne := _, eq_zero_or_eq_zero_of_mul_eq_zero := _}

source

@[class]

structure field :

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
inv : α → α
exists_pair_ne : ∃ (x y : α), x ≠ y
mul_inv_cancel : ∀ {a : α}, a ≠ 0 → a * a⁻¹ = 1
inv_zero : 0⁻¹ = 0

A field is a comm_ring with multiplicative inverses for nonzero elements

Instances

source

@[instance]

def field.to_has_inv (α : Type u) [s : field α] :

has_inv α

source

@[instance]

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

comm_ring α

source

@[instance]

def field.to_nontrivial (α : Type u) [s : field α] :

nontrivial α

source

@[instance]

def field.to_division_ring {α : Type u} [field α] :

division_ring α

Equations

field.to_division_ring = {add := field.add (show field α, from _inst_1), add_assoc := _, zero := field.zero (show field α, from _inst_1), zero_add := _, add_zero := _, neg := field.neg (show field α, from _inst_1), add_left_neg := _, add_comm := _, mul := field.mul (show field α, from _inst_1), mul_assoc := _, one := field.one (show field α, from _inst_1), one_mul := _, mul_one := _, left_distrib := _, right_distrib := _, inv := field.inv (show field α, from _inst_1), exists_pair_ne := _, mul_inv_cancel := _, inv_mul_cancel := _, inv_zero := _}

source

@[instance]

def field.to_comm_group_with_zero {α : Type u} [field α] :

comm_group_with_zero α

Every field is a comm_group_with_zero.

Equations

field.to_comm_group_with_zero = {mul := group_with_zero.mul division_ring.to_group_with_zero, mul_assoc := _, one := group_with_zero.one division_ring.to_group_with_zero, one_mul := _, mul_one := _, mul_comm := _, zero := group_with_zero.zero division_ring.to_group_with_zero, zero_mul := _, mul_zero := _, inv := group_with_zero.inv division_ring.to_group_with_zero, exists_pair_ne := _, inv_zero := _, mul_inv_cancel := _}

source

theorem one_div_add_one_div {α : Type u} [field α] {a b : α} :

a ≠ 0 → b ≠ 0 → 1 / a + 1 / b = (a + b) / (a * b)

source

theorem div_add_div {α : Type u} [field α] (a : α) {b : α} (c : α) {d : α} :

b ≠ 0 → d ≠ 0 → a / b + c / d = (a * d + b * c) / (b * d)

source

theorem div_sub_div {α : Type u} [field α] (a : α) {b : α} (c : α) {d : α} :

b ≠ 0 → d ≠ 0 → a / b - c / d = (a * d - b * c) / (b * d)

source

theorem inv_add_inv {α : Type u} [field α] {a b : α} :

a ≠ 0 → b ≠ 0 → a⁻¹ + b⁻¹ = (a + b) / (a * b)

source

theorem inv_sub_inv {α : Type u} [field α] {a b : α} :

a ≠ 0 → b ≠ 0 → a⁻¹ - b⁻¹ = (b - a) / (a * b)

source

theorem add_div' {α : Type u} [field α] (a b c : α) :

c ≠ 0 → b + a / c = (b * c + a) / c

source

theorem sub_div' {α : Type u} [field α] (a b c : α) :

c ≠ 0 → b - a / c = (b * c - a) / c

source

theorem div_add' {α : Type u} [field α] (a b c : α) :

c ≠ 0 → a / c + b = (a + b * c) / c

source

theorem div_sub' {α : Type u} [field α] (a b c : α) :

c ≠ 0 → a / c - b = (a - c * b) / c

source

@[instance]

def field.to_integral_domain {α : Type u} [field α] :

integral_domain α

Equations

field.to_integral_domain = {add := field.add _inst_1, add_assoc := _, zero := field.zero _inst_1, zero_add := _, add_zero := _, neg := field.neg _inst_1, add_left_neg := _, add_comm := _, mul := field.mul _inst_1, mul_assoc := _, one := field.one _inst_1, one_mul := _, mul_one := _, left_distrib := _, right_distrib := _, mul_comm := _, exists_pair_ne := _, eq_zero_or_eq_zero_of_mul_eq_zero := _}

source

@[simp]

theorem ring_hom.map_units_inv {R : Type u_1} {K : Type u_2} [semiring R] [division_ring K] (f : R →+* K) (u : units R) :

⇑f ↑u⁻¹ = (⇑f ↑u)⁻¹

source

theorem ring_hom.map_ne_zero {α : Type u} {β : Type u_1} [division_ring α] [semiring β] [nontrivial β] (f : α →+* β) {x : α} :

⇑f x ≠ 0 ↔ x ≠ 0

source

theorem ring_hom.map_eq_zero {α : Type u} {β : Type u_1} [division_ring α] [semiring β] [nontrivial β] (f : α →+* β) {x : α} :

⇑f x = 0 ↔ x = 0

source

theorem ring_hom.map_inv {α : Type u} {γ : Type u_2} [division_ring α] [division_ring γ] (g : α →+* γ) (x : α) :

⇑g x⁻¹ = (⇑g x)⁻¹

source

theorem ring_hom.map_div {α : Type u} {γ : Type u_2} [division_ring α] [division_ring γ] (g : α →+* γ) (x y : α) :

⇑g (x / y) = ⇑g x / ⇑g y

source

theorem ring_hom.injective {α : Type u} {β : Type u_1} [division_ring α] [semiring β] [nontrivial β] (f : α →+* β) :

function.injective ⇑f

mathlib documentation

algebra.field

General documentation

Additional documentation

Library

mathlib documentation

algebra.​field

General documentation

Additional documentation

Library

algebra.field