mathlib documentation

algebra.field

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

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

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

A division_ring is a ring with multiplicative inverses for nonzero elements

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

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

Equations
@[instance]

Every division ring is a group_with_zero.

Equations
theorem inv_eq_one_div {α : Type u} [division_ring α] (a : α) :
a⁻¹ = 1 / a

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

theorem one_div_neg_one_eq_neg_one {α : Type u} [division_ring α] :
1 / -1 = -1

theorem one_div_neg_eq_neg_one_div {α : Type u} [division_ring α] (a : α) :
1 / -a = -(1 / a)

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

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

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

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

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

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

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

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

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

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

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

theorem one_div_mul_add_mul_one_div_eq_one_div_add_one_div {α : Type u} [division_ring α] {a b : α} :
a 0b 0((1 / a) * (a + b)) * (1 / b) = 1 / a + 1 / b

theorem one_div_mul_sub_mul_one_div_eq_one_div_add_one_div {α : Type u} [division_ring α] {a b : α} :
a 0b 0((1 / a) * (b - a)) * (1 / b) = 1 / a - 1 / b

theorem add_div_eq_mul_add_div {α : Type u} [division_ring α] (a b : α) {c : α} :
c 0a + b / c = (a * c + b) / c

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

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

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

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

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

A field is a comm_ring with multiplicative inverses for nonzero elements

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

Equations
theorem one_div_add_one_div {α : Type u} [field α] {a b : α} :
a 0b 01 / a + 1 / b = (a + b) / a * b

theorem div_add_div {α : Type u} [field α] (a : α) {b : α} (c : α) {d : α} :
b 0d 0a / b + c / d = (a * d + b * c) / b * d

theorem div_sub_div {α : Type u} [field α] (a : α) {b : α} (c : α) {d : α} :
b 0d 0a / b - c / d = (a * d - b * c) / b * d

theorem inv_add_inv {α : Type u} [field α] {a b : α} :
a 0b 0a⁻¹ + b⁻¹ = (a + b) / a * b

theorem inv_sub_inv {α : Type u} [field α] {a b : α} :
a 0b 0a⁻¹ - b⁻¹ = (b - a) / a * b

theorem add_div' {α : Type u} [field α] (a b c : α) :
c 0b + a / c = (b * c + a) / c

theorem sub_div' {α : Type u} [field α] (a b c : α) :
c 0b - a / c = (b * c - a) / c

theorem div_add' {α : Type u} [field α] (a b c : α) :
c 0a / c + b = (a + b * c) / c

theorem div_sub' {α : Type u} [field α] (a b c : α) :
c 0a / c - b = (a - c * b) / c

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

Equations
structure is_field (R : Type u) [ring R] :
Prop
  • exists_pair_ne : ∃ (x y : R), x y
  • mul_comm : ∀ (x y : R), x * y = y * x
  • mul_inv_cancel : ∀ {a : R}, a 0(∃ (b : R), a * b = 1)

A predicate to express that a ring is a field.

This is mainly useful because such a predicate does not contain data, and can therefore be easily transported along ring isomorphisms. Additionaly, this is useful when trying to prove that a particular ring structure extends to a field.

theorem field.to_is_field (R : Type u) [field R] :

Transferring from field to is_field

def is_field.to_field (R : Type u) [ring R] :
is_field Rfield R

Transferring from is_field to field

Equations
theorem uniq_inv_of_is_field (R : Type u) [ring R] (hf : is_field R) (x : R) :
x 0(∃! (y : R), x * y = 1)

For each field, and for each nonzero element of said field, there is a unique inverse. Since is_field doesn't remember the data of an inv function and as such, a lemma that there is a unique inverse could be useful.

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

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

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

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

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

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