algebra.field

# Fields and division rings #

This file introduces fields and division rings (also known as skewfields) and proves some basic statements about them. For a more extensive theory of fields, see the field_theory folder.

## Main definitions #

• division_ring: introduces the notion of a division ring as a ring such that 0 ≠ 1 and a * a⁻¹ = 1 for a ≠ 0
• field: a division ring which is also a commutative ring.
• is_field: a predicate on a ring that it is a field, i.e. that the multiplication is commutative, that it has more than one element and that all non-zero elements have a multiplicative inverse. In contrast to field, which contains the data of a function associating to an element of the field its multiplicative inverse, this predicate only assumes the existence and can therefore more easily be used to e.g. transfer along ring isomorphisms.

## Implementation details #

By convention 0⁻¹ = 0 in a field or division ring. This is due to the fact that working with total functions has the advantage of not constantly having to check that x ≠ 0 when writing x⁻¹. With this convention in place, some statements like (a + b) * c⁻¹ = a * c⁻¹ + b * c⁻¹ still remain true, while others like the defining property a * a⁻¹ = 1 need the assumption a ≠ 0. If you are a beginner in using Lean and are confused by that, you can read more about why this convention is taken in Kevin Buzzard's blogpost

A division ring or field is an example of a group_with_zero. If you cannot find a division ring / field lemma that does not involve +, you can try looking for a group_with_zero lemma instead.

## Tags #

field, division ring, skew field, skew-field, skewfield

@[instance]
def division_ring.to_nontrivial (K : Type u) [self : division_ring K] :
@[instance]
def division_ring.to_div_inv_monoid (K : Type u) [self : division_ring K] :
@[class]
structure division_ring (K : Type u) :
Type u
• add : K → K → K
• add_assoc : ∀ (a b c_1 : K), a + b + c_1 = a + (b + c_1)
• zero : K
• zero_add : ∀ (a : K), 0 + a = a
• add_zero : ∀ (a : K), a + 0 = a
• nsmul : K → K
• nsmul_zero' : (∀ (x : K), = 0) . "try_refl_tac"
• nsmul_succ' : (∀ (n : ) (x : K), = x + . "try_refl_tac"
• neg : K → K
• sub : K → K → K
• sub_eq_add_neg : (∀ (a b : K), a - b = a + -b) . "try_refl_tac"
• gsmul : K → K
• gsmul_zero' : (∀ (a : K), = 0) . "try_refl_tac"
• gsmul_succ' : (∀ (n : ) (a : K), = a + . "try_refl_tac"
• gsmul_neg' : (∀ (n : ) (a : K), = - a) . "try_refl_tac"
• add_left_neg : ∀ (a : K), -a + a = 0
• add_comm : ∀ (a b : K), a + b = b + a
• mul : K → K → K
• mul_assoc : ∀ (a b c_1 : K), (a * b) * c_1 = a * b * c_1
• one : K
• one_mul : ∀ (a : K), 1 * a = a
• mul_one : ∀ (a : K), a * 1 = a
• npow : K → K
• npow_zero' : (∀ (x : K), = 1) . "try_refl_tac"
• npow_succ' : (∀ (n : ) (x : K), = x * . "try_refl_tac"
• left_distrib : ∀ (a b c_1 : K), a * (b + c_1) = a * b + a * c_1
• right_distrib : ∀ (a b c_1 : K), (a + b) * c_1 = a * c_1 + b * c_1
• inv : K → K
• div : K → K → K
• div_eq_mul_inv : (∀ (a b : K), a / b = a * b⁻¹) . "try_refl_tac"
• gpow : K → K
• gpow_zero' : (∀ (a : K), = 1) . "try_refl_tac"
• gpow_succ' : (∀ (n : ) (a : K), = a * a) . "try_refl_tac"
• gpow_neg' : (∀ (n : ) (a : K), = a)⁻¹) . "try_refl_tac"
• exists_pair_ne : ∃ (x y : K), x y
• mul_inv_cancel : ∀ {a : K}, 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 (K : Type u) [self : division_ring K] :
@[protected, instance]
def division_ring.to_group_with_zero {K : Type u}  :

Every division ring is a group_with_zero.

Equations
theorem inverse_eq_has_inv {K : Type u}  :
theorem one_div_neg_one_eq_neg_one {K : Type u}  :
1 / -1 = -1
theorem one_div_neg_eq_neg_one_div {K : Type u} (a : K) :
1 / -a = -(1 / a)
theorem div_neg_eq_neg_div {K : Type u} (a b : K) :
b / -a = -(b / a)
theorem neg_div {K : Type u} (a b : K) :
-b / a = -(b / a)
theorem neg_div' {K : Type u_1} (a b : K) :
-(b / a) = -b / a
theorem neg_div_neg_eq {K : Type u} (a b : K) :
-a / -b = a / b
theorem div_add_div_same {K : Type u} (a b c : K) :
a / c + b / c = (a + b) / c
theorem same_add_div {K : Type u} {a b : K} (h : b 0) :
(b + a) / b = 1 + a / b
theorem one_add_div {K : Type u} {a b : K} (h : b 0) :
1 + a / b = (b + a) / b
theorem div_add_same {K : Type u} {a b : K} (h : b 0) :
(a + b) / b = a / b + 1
theorem div_add_one {K : Type u} {a b : K} (h : b 0) :
a / b + 1 = (a + b) / b
theorem div_sub_div_same {K : Type u} (a b c : K) :
a / c - b / c = (a - b) / c
theorem same_sub_div {K : Type u} {a b : K} (h : b 0) :
(b - a) / b = 1 - a / b
theorem one_sub_div {K : Type u} {a b : K} (h : b 0) :
1 - a / b = (b - a) / b
theorem div_sub_same {K : Type u} {a b : K} (h : b 0) :
(a - b) / b = a / b - 1
theorem div_sub_one {K : Type u} {a b : K} (h : b 0) :
a / b - 1 = (a - b) / b
theorem neg_inv {K : Type u} {a : K} :
theorem add_div {K : Type u} (a b c : K) :
(a + b) / c = a / c + b / c
theorem sub_div {K : Type u} (a b c : K) :
(a - b) / c = a / c - b / c
theorem div_neg {K : Type u} {b : K} (a : K) :
a / -b = -(a / b)
theorem inv_neg {K : Type u} {a : K} :
theorem one_div_mul_add_mul_one_div_eq_one_div_add_one_div {K : Type u} {a b : K} (ha : a 0) (hb : b 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 {K : Type u} {a b : K} (ha : a 0) (hb : b 0) :
((1 / a) * (b - a)) * (1 / b) = 1 / a - 1 / b
theorem add_div_eq_mul_add_div {K : Type u} (a b : K) {c : K} (hc : c 0) :
a + b / c = (a * c + b) / c
@[protected, instance]
def division_ring.to_domain {K : Type u}  :
Equations
@[instance]
def field.to_div_inv_monoid (K : Type u) [self : field K] :
@[instance]
def field.to_comm_ring (K : Type u) [self : field K] :
@[instance]
def field.to_nontrivial (K : Type u) [self : field K] :
@[class]
structure field (K : Type u) :
Type u
• add : K → K → K
• add_assoc : ∀ (a b c_1 : K), a + b + c_1 = a + (b + c_1)
• zero : K
• zero_add : ∀ (a : K), 0 + a = a
• add_zero : ∀ (a : K), a + 0 = a
• nsmul : K → K
• nsmul_zero' : (∀ (x : K), x = 0) . "try_refl_tac"
• nsmul_succ' : (∀ (n : ) (x : K), x = x + x) . "try_refl_tac"
• neg : K → K
• sub : K → K → K
• sub_eq_add_neg : (∀ (a b : K), a - b = a + -b) . "try_refl_tac"
• gsmul : K → K
• gsmul_zero' : (∀ (a : K), a = 0) . "try_refl_tac"
• gsmul_succ' : (∀ (n : ) (a : K), a = a + a) . "try_refl_tac"
• gsmul_neg' : (∀ (n : ) (a : K), a = -field.gsmul (n.succ) a) . "try_refl_tac"
• add_left_neg : ∀ (a : K), -a + a = 0
• add_comm : ∀ (a b : K), a + b = b + a
• mul : K → K → K
• mul_assoc : ∀ (a b c_1 : K), (a * b) * c_1 = a * b * c_1
• one : K
• one_mul : ∀ (a : K), 1 * a = a
• mul_one : ∀ (a : K), a * 1 = a
• npow : K → K
• npow_zero' : (∀ (x : K), x = 1) . "try_refl_tac"
• npow_succ' : (∀ (n : ) (x : K), x = x * x) . "try_refl_tac"
• left_distrib : ∀ (a b c_1 : K), a * (b + c_1) = a * b + a * c_1
• right_distrib : ∀ (a b c_1 : K), (a + b) * c_1 = a * c_1 + b * c_1
• mul_comm : ∀ (a b : K), a * b = b * a
• inv : K → K
• div : K → K → K
• div_eq_mul_inv : (∀ (a b : K), a / b = a * b⁻¹) . "try_refl_tac"
• gpow : K → K
• gpow_zero' : (∀ (a : K), a = 1) . "try_refl_tac"
• gpow_succ' : (∀ (n : ) (a : K), a = a * a) . "try_refl_tac"
• gpow_neg' : (∀ (n : ) (a : K), a = (field.gpow (n.succ) a)⁻¹) . "try_refl_tac"
• exists_pair_ne : ∃ (x y : K), x y
• mul_inv_cancel : ∀ {a : K}, a 0a * a⁻¹ = 1
• inv_zero : 0⁻¹ = 0

A field is a comm_ring with multiplicative inverses for nonzero elements

Instances
@[protected, instance]
def field.to_division_ring {K : Type u} [field K] :
Equations
@[protected, instance]
def field.to_comm_group_with_zero {K : Type u} [field K] :

Every field is a comm_group_with_zero.

Equations
theorem div_add_div {K : Type u} [field K] (a : K) {b : K} (c : K) {d : K} (hb : b 0) (hd : d 0) :
a / b + c / d = (a * d + b * c) / b * d
theorem one_div_add_one_div {K : Type u} [field K] {a b : K} (ha : a 0) (hb : b 0) :
1 / a + 1 / b = (a + b) / a * b
theorem div_sub_div {K : Type u} [field K] (a : K) {b : K} (c : K) {d : K} (hb : b 0) (hd : d 0) :
a / b - c / d = (a * d - b * c) / b * d
theorem inv_add_inv {K : Type u} [field K] {a b : K} (ha : a 0) (hb : b 0) :
a⁻¹ + b⁻¹ = (a + b) / a * b
theorem inv_sub_inv {K : Type u} [field K] {a b : K} (ha : a 0) (hb : b 0) :
a⁻¹ - b⁻¹ = (b - a) / a * b
theorem add_div' {K : Type u} [field K] (a b c : K) (hc : c 0) :
b + a / c = (b * c + a) / c
theorem sub_div' {K : Type u} [field K] (a b c : K) (hc : c 0) :
b - a / c = (b * c - a) / c
theorem div_add' {K : Type u} [field K] (a b c : K) (hc : c 0) :
a / c + b = (a + b * c) / c
theorem div_sub' {K : Type u} [field K] (a b c : K) (hc : c 0) :
a / c - b = (a - c * b) / c
@[protected, instance]
def field.to_integral_domain {K : Type u} [field K] :
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] (h : is_field 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 {K : Type u} {R : Type u_1} [semiring R] (f : R →+* K) (u : units R) :
theorem ring_hom.map_ne_zero {K : Type u} {R : Type u_1} [semiring R] [nontrivial R] (f : K →+* R) {x : K} :
f x 0 x 0
@[simp]
theorem ring_hom.map_eq_zero {K : Type u} {R : Type u_1} [semiring R] [nontrivial R] (f : K →+* R) {x : K} :
f x = 0 x = 0
theorem ring_hom.map_inv {K : Type u} {K' : Type u_2} [division_ring K'] (g : K →+* K') (x : K) :
theorem ring_hom.map_div {K : Type u} {K' : Type u_2} [division_ring K'] (g : K →+* K') (x y : K) :
g (x / y) = g x / g y
@[protected]
theorem ring_hom.injective {K : Type u} {R : Type u_1} [semiring R] [nontrivial R] (f : K →+* R) :
def division_ring_of_is_unit_or_eq_zero {R : Type u_1} [nontrivial R] [hR : ring R] (h : ∀ (a : R), a = 0) :

Constructs a division_ring structure on a ring consisting only of units and 0.

Equations
def field_of_is_unit_or_eq_zero {R : Type u_1} [nontrivial R] [hR : comm_ring R] (h : ∀ (a : R), a = 0) :

Constructs a field structure on a comm_ring consisting only of units and 0.

Equations
@[protected]
def function.injective.division_ring {K : Type u} {K' : Type u_1} [has_zero K'] [has_mul K'] [has_add K'] [has_neg K'] [has_sub K'] [has_one K'] [has_inv K'] [has_div K'] (f : K' → K) (hf : function.injective f) (zero : f 0 = 0) (one : f 1 = 1) (add : ∀ (x y : K'), f (x + y) = f x + f y) (mul : ∀ (x y : K'), f (x * y) = (f x) * f y) (neg : ∀ (x : K'), f (-x) = -f x) (sub : ∀ (x y : K'), f (x - y) = f x - f y) (inv : ∀ (x : K'), f x⁻¹ = (f x)⁻¹) (div : ∀ (x y : K'), f (x / y) = f x / f y) :

Pullback a division_ring along an injective function.

Equations
@[protected]
def function.injective.field {K : Type u} [field K] {K' : Type u_1} [has_zero K'] [has_mul K'] [has_add K'] [has_neg K'] [has_sub K'] [has_one K'] [has_inv K'] [has_div K'] (f : K' → K) (hf : function.injective f) (zero : f 0 = 0) (one : f 1 = 1) (add : ∀ (x y : K'), f (x + y) = f x + f y) (mul : ∀ (x y : K'), f (x * y) = (f x) * f y) (neg : ∀ (x : K'), f (-x) = -f x) (sub : ∀ (x y : K'), f (x - y) = f x - f y) (inv : ∀ (x : K'), f x⁻¹ = (f x)⁻¹) (div : ∀ (x y : K'), f (x / y) = f x / f y) :

Pullback a field along an injective function.

Equations