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 aring
such that0 ≠ 1
anda * a⁻¹ = 1
fora ≠ 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 tofield
, 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
- 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), division_ring.nsmul 0 x = 0) . "try_refl_tac"
- nsmul_succ' : (∀ (n : ℕ) (x : K), division_ring.nsmul n.succ x = x + division_ring.nsmul n 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), division_ring.gsmul 0 a = 0) . "try_refl_tac"
- gsmul_succ' : (∀ (n : ℕ) (a : K), division_ring.gsmul (int.of_nat n.succ) a = a + division_ring.gsmul (int.of_nat n) a) . "try_refl_tac"
- gsmul_neg' : (∀ (n : ℕ) (a : K), division_ring.gsmul -[1+ n] a = -division_ring.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), division_ring.npow 0 x = 1) . "try_refl_tac"
- npow_succ' : (∀ (n : ℕ) (x : K), division_ring.npow n.succ x = x * division_ring.npow n 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), division_ring.gpow 0 a = 1) . "try_refl_tac"
- gpow_succ' : (∀ (n : ℕ) (a : K), division_ring.gpow (int.of_nat n.succ) a = a * division_ring.gpow (int.of_nat n) a) . "try_refl_tac"
- gpow_neg' : (∀ (n : ℕ) (a : K), division_ring.gpow -[1+ n] a = (division_ring.gpow ↑(n.succ) a)⁻¹) . "try_refl_tac"
- exists_pair_ne : ∃ (x y : K), x ≠ y
- mul_inv_cancel : ∀ {a : K}, a ≠ 0 → a * a⁻¹ = 1
- inv_zero : 0⁻¹ = 0
A division_ring
is a ring
with multiplicative inverses for nonzero elements
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 := _, npow := division_ring.npow _inst_1, npow_zero' := _, npow_succ' := _, zero := division_ring.zero _inst_1, zero_mul := _, mul_zero := _, inv := division_ring.inv _inst_1, div := division_ring.div _inst_1, div_eq_mul_inv := _, gpow := division_ring.gpow _inst_1, gpow_zero' := _, gpow_succ' := _, gpow_neg' := _, exists_pair_ne := _, inv_zero := _, mul_inv_cancel := _}
Equations
- division_ring.to_domain = {add := division_ring.add _inst_1, add_assoc := _, zero := division_ring.zero _inst_1, zero_add := _, add_zero := _, nsmul := division_ring.nsmul _inst_1, nsmul_zero' := _, nsmul_succ' := _, neg := division_ring.neg _inst_1, sub := division_ring.sub _inst_1, sub_eq_add_neg := _, gsmul := division_ring.gsmul _inst_1, gsmul_zero' := _, gsmul_succ' := _, gsmul_neg' := _, add_left_neg := _, add_comm := _, mul := division_ring.mul _inst_1, mul_assoc := _, one := division_ring.one _inst_1, one_mul := _, mul_one := _, npow := division_ring.npow _inst_1, npow_zero' := _, npow_succ' := _, left_distrib := _, right_distrib := _, exists_pair_ne := _, eq_zero_or_eq_zero_of_mul_eq_zero := _}
- 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), field.nsmul 0 x = 0) . "try_refl_tac"
- nsmul_succ' : (∀ (n : ℕ) (x : K), field.nsmul n.succ x = x + field.nsmul n 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), field.gsmul 0 a = 0) . "try_refl_tac"
- gsmul_succ' : (∀ (n : ℕ) (a : K), field.gsmul (int.of_nat n.succ) a = a + field.gsmul (int.of_nat n) a) . "try_refl_tac"
- gsmul_neg' : (∀ (n : ℕ) (a : K), field.gsmul -[1+ n] 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), field.npow 0 x = 1) . "try_refl_tac"
- npow_succ' : (∀ (n : ℕ) (x : K), field.npow n.succ x = x * field.npow n 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), field.gpow 0 a = 1) . "try_refl_tac"
- gpow_succ' : (∀ (n : ℕ) (a : K), field.gpow (int.of_nat n.succ) a = a * field.gpow (int.of_nat n) a) . "try_refl_tac"
- gpow_neg' : (∀ (n : ℕ) (a : K), field.gpow -[1+ n] a = (field.gpow ↑(n.succ) a)⁻¹) . "try_refl_tac"
- exists_pair_ne : ∃ (x y : K), x ≠ y
- mul_inv_cancel : ∀ {a : K}, a ≠ 0 → a * a⁻¹ = 1
- inv_zero : 0⁻¹ = 0
A field
is a comm_ring
with multiplicative inverses for nonzero elements
Instances
- linear_ordered_field.to_field
- normed_field.to_field
- opposite.field
- rat.field
- local_ring.residue_field.field
- localization_map.codomain.field
- fraction_ring.field
- adjoin_root.field
- polynomial.splitting_field_aux.field
- polynomial.splitting_field.field
- algebraic_closure.adjoin_monic.field
- algebraic_closure.step.field
- algebraic_closure.field
- zmod.field
- real.field
- complex.field
- padic.field
- filter.germ.field
- is_subfield.field
- subfield.to_field
- intermediate_field.to_field
- perfect_closure.field
- tilt.field
Equations
- field.to_division_ring = {add := field.add (show field K, from _inst_1), add_assoc := _, zero := field.zero (show field K, from _inst_1), zero_add := _, add_zero := _, nsmul := field.nsmul (show field K, from _inst_1), nsmul_zero' := _, nsmul_succ' := _, neg := field.neg (show field K, from _inst_1), sub := field.sub (show field K, from _inst_1), sub_eq_add_neg := _, gsmul := field.gsmul (show field K, from _inst_1), gsmul_zero' := _, gsmul_succ' := _, gsmul_neg' := _, add_left_neg := _, add_comm := _, mul := field.mul (show field K, from _inst_1), mul_assoc := _, one := field.one (show field K, from _inst_1), one_mul := _, mul_one := _, npow := field.npow (show field K, from _inst_1), npow_zero' := _, npow_succ' := _, left_distrib := _, right_distrib := _, inv := field.inv (show field K, from _inst_1), div := field.div (show field K, from _inst_1), div_eq_mul_inv := _, gpow := field.gpow (show field K, from _inst_1), gpow_zero' := _, gpow_succ' := _, gpow_neg' := _, exists_pair_ne := _, mul_inv_cancel := _, inv_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 := _, npow := group_with_zero.npow division_ring.to_group_with_zero, npow_zero' := _, npow_succ' := _, 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, div := group_with_zero.div division_ring.to_group_with_zero, div_eq_mul_inv := _, gpow := group_with_zero.gpow division_ring.to_group_with_zero, gpow_zero' := _, gpow_succ' := _, gpow_neg' := _, exists_pair_ne := _, inv_zero := _, mul_inv_cancel := _}
Equations
- field.to_integral_domain = {add := field.add _inst_1, add_assoc := _, zero := field.zero _inst_1, zero_add := _, add_zero := _, nsmul := field.nsmul _inst_1, nsmul_zero' := _, nsmul_succ' := _, neg := field.neg _inst_1, sub := field.sub _inst_1, sub_eq_add_neg := _, gsmul := field.gsmul _inst_1, gsmul_zero' := _, gsmul_succ' := _, gsmul_neg' := _, add_left_neg := _, add_comm := _, mul := field.mul _inst_1, mul_assoc := _, one := field.one _inst_1, one_mul := _, mul_one := _, npow := field.npow _inst_1, npow_zero' := _, npow_succ' := _, left_distrib := _, right_distrib := _, mul_comm := _, exists_pair_ne := _, eq_zero_or_eq_zero_of_mul_eq_zero := _}
- 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.
Transferring from field to is_field
Transferring from is_field to field
Equations
- is_field.to_field R h = {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' := _, neg := ring.neg _inst_1, sub := ring.sub _inst_1, sub_eq_add_neg := _, gsmul := ring.gsmul _inst_1, gsmul_zero' := _, gsmul_succ' := _, gsmul_neg' := _, add_left_neg := _, 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' := _, left_distrib := _, right_distrib := _, mul_comm := _, inv := λ (a : R), dite (a = 0) (λ (ha : a = 0), 0) (λ (ha : ¬a = 0), classical.some _), div := div_inv_monoid.div._default ring.mul ring.mul_assoc ring.one ring.one_mul ring.mul_one ring.npow ring.npow_zero' ring.npow_succ' (λ (a : R), dite (a = 0) (λ (ha : a = 0), 0) (λ (ha : ¬a = 0), classical.some _)), div_eq_mul_inv := _, gpow := div_inv_monoid.gpow._default ring.mul ring.mul_assoc ring.one ring.one_mul ring.mul_one ring.npow ring.npow_zero' ring.npow_succ' (λ (a : R), dite (a = 0) (λ (ha : a = 0), 0) (λ (ha : ¬a = 0), classical.some _)), gpow_zero' := _, gpow_succ' := _, gpow_neg' := _, exists_pair_ne := _, mul_inv_cancel := _, inv_zero := _}
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.
Constructs a division_ring
structure on a ring
consisting only of units and 0.
Equations
- division_ring_of_is_unit_or_eq_zero h = {add := ring.add hR, add_assoc := _, zero := group_with_zero.zero (group_with_zero_of_is_unit_or_eq_zero h), zero_add := _, add_zero := _, nsmul := ring.nsmul hR, nsmul_zero' := _, nsmul_succ' := _, neg := ring.neg hR, sub := ring.sub hR, sub_eq_add_neg := _, gsmul := ring.gsmul hR, gsmul_zero' := _, gsmul_succ' := _, gsmul_neg' := _, add_left_neg := _, add_comm := _, mul := group_with_zero.mul (group_with_zero_of_is_unit_or_eq_zero h), mul_assoc := _, one := group_with_zero.one (group_with_zero_of_is_unit_or_eq_zero h), one_mul := _, mul_one := _, npow := group_with_zero.npow (group_with_zero_of_is_unit_or_eq_zero h), npow_zero' := _, npow_succ' := _, left_distrib := _, right_distrib := _, inv := group_with_zero.inv (group_with_zero_of_is_unit_or_eq_zero h), div := group_with_zero.div (group_with_zero_of_is_unit_or_eq_zero h), div_eq_mul_inv := _, gpow := group_with_zero.gpow (group_with_zero_of_is_unit_or_eq_zero h), gpow_zero' := _, gpow_succ' := _, gpow_neg' := _, exists_pair_ne := _, mul_inv_cancel := _, inv_zero := _}
Constructs a field
structure on a comm_ring
consisting only of units and 0.
Equations
- field_of_is_unit_or_eq_zero h = {add := comm_ring.add hR, add_assoc := _, zero := group_with_zero.zero (group_with_zero_of_is_unit_or_eq_zero h), zero_add := _, add_zero := _, nsmul := comm_ring.nsmul hR, nsmul_zero' := _, nsmul_succ' := _, neg := comm_ring.neg hR, sub := comm_ring.sub hR, sub_eq_add_neg := _, gsmul := comm_ring.gsmul hR, gsmul_zero' := _, gsmul_succ' := _, gsmul_neg' := _, add_left_neg := _, add_comm := _, mul := group_with_zero.mul (group_with_zero_of_is_unit_or_eq_zero h), mul_assoc := _, one := group_with_zero.one (group_with_zero_of_is_unit_or_eq_zero h), one_mul := _, mul_one := _, npow := group_with_zero.npow (group_with_zero_of_is_unit_or_eq_zero h), npow_zero' := _, npow_succ' := _, left_distrib := _, right_distrib := _, mul_comm := _, inv := group_with_zero.inv (group_with_zero_of_is_unit_or_eq_zero h), div := group_with_zero.div (group_with_zero_of_is_unit_or_eq_zero h), div_eq_mul_inv := _, gpow := group_with_zero.gpow (group_with_zero_of_is_unit_or_eq_zero h), gpow_zero' := _, gpow_succ' := _, gpow_neg' := _, exists_pair_ne := _, mul_inv_cancel := _, inv_zero := _}
Pullback a division_ring
along an injective function.
Equations
- function.injective.division_ring f hf zero one add mul neg sub inv div = {add := ring.add (function.injective.ring f hf zero one add mul neg sub), add_assoc := _, zero := group_with_zero.zero (function.injective.group_with_zero f hf zero one mul inv div), 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 := _, gsmul := ring.gsmul (function.injective.ring f hf zero one add mul neg sub), gsmul_zero' := _, gsmul_succ' := _, gsmul_neg' := _, add_left_neg := _, add_comm := _, mul := group_with_zero.mul (function.injective.group_with_zero f hf zero one mul inv div), mul_assoc := _, one := group_with_zero.one (function.injective.group_with_zero f hf zero one mul inv div), one_mul := _, mul_one := _, npow := group_with_zero.npow (function.injective.group_with_zero f hf zero one mul inv div), npow_zero' := _, npow_succ' := _, left_distrib := _, right_distrib := _, inv := group_with_zero.inv (function.injective.group_with_zero f hf zero one mul inv div), div := group_with_zero.div (function.injective.group_with_zero f hf zero one mul inv div), div_eq_mul_inv := _, gpow := group_with_zero.gpow (function.injective.group_with_zero f hf zero one mul inv div), gpow_zero' := _, gpow_succ' := _, gpow_neg' := _, exists_pair_ne := _, mul_inv_cancel := _, inv_zero := _}
Pullback a field
along an injective function.
Equations
- function.injective.field f hf zero one add mul neg sub inv div = {add := comm_ring.add (function.injective.comm_ring f hf zero one add mul neg sub), add_assoc := _, zero := comm_group_with_zero.zero (function.injective.comm_group_with_zero f hf zero one mul inv div), 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 := _, gsmul := comm_ring.gsmul (function.injective.comm_ring f hf zero one add mul neg sub), gsmul_zero' := _, gsmul_succ' := _, gsmul_neg' := _, add_left_neg := _, add_comm := _, mul := comm_group_with_zero.mul (function.injective.comm_group_with_zero f hf zero one mul inv div), mul_assoc := _, one := comm_group_with_zero.one (function.injective.comm_group_with_zero f hf zero one mul inv div), one_mul := _, mul_one := _, npow := comm_group_with_zero.npow (function.injective.comm_group_with_zero f hf zero one mul inv div), npow_zero' := _, npow_succ' := _, left_distrib := _, right_distrib := _, mul_comm := _, inv := comm_group_with_zero.inv (function.injective.comm_group_with_zero f hf zero one mul inv div), div := comm_group_with_zero.div (function.injective.comm_group_with_zero f hf zero one mul inv div), div_eq_mul_inv := _, gpow := comm_group_with_zero.gpow (function.injective.comm_group_with_zero f hf zero one mul inv div), gpow_zero' := _, gpow_succ' := _, gpow_neg' := _, exists_pair_ne := _, mul_inv_cancel := _, inv_zero := _}