mathlib documentation

algebra.field.basic

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

div_inv_monoid K

@[class]

structure division_ring (K : Type u) :

Type u

add : K → K → K
add_assoc : ∀ (a b c : K), a + b + c = a + (b + c)
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"
zsmul : ℤ → K → K
zsmul_zero' : (∀ (a : K), division_ring.zsmul 0 a = 0) . "try_refl_tac"
zsmul_succ' : (∀ (n : ℕ) (a : K), division_ring.zsmul (int.of_nat n.succ) a = a + division_ring.zsmul (int.of_nat n) a) . "try_refl_tac"
zsmul_neg' : (∀ (n : ℕ) (a : K), division_ring.zsmul -[1+ n] a = -division_ring.zsmul ↑(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 : K), (a * b) * c = a * b * c
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 : K), a * (b + c) = a * b + a * c
right_distrib : ∀ (a b c : K), (a + b) * c = a * c + b * c
inv : K → K
div : K → K → K
div_eq_mul_inv : (∀ (a b : K), a / b = a * b⁻¹) . "try_refl_tac"
zpow : ℤ → K → K
zpow_zero' : (∀ (a : K), division_ring.zpow 0 a = 1) . "try_refl_tac"
zpow_succ' : (∀ (n : ℕ) (a : K), division_ring.zpow (int.of_nat n.succ) a = a * division_ring.zpow (int.of_nat n) a) . "try_refl_tac"
zpow_neg' : (∀ (n : ℕ) (a : K), division_ring.zpow -[1+ n] a = (division_ring.zpow ↑(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

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} [division_ring K] :

group_with_zero K

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 := _, zpow := division_ring.zpow _inst_1, zpow_zero' := _, zpow_succ' := _, zpow_neg' := _, exists_pair_ne := _, inv_zero := _, mul_inv_cancel := _}

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

1 / -1 = -1

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

1 / -a = -(1 / a)

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

b / -a = -(b / a)

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

-b / a = -(b / a)

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

-(b / a) = -b / a

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

-a / -b = a / b

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

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

theorem same_add_div {K : Type u} [division_ring K] {a b : K} (h : b ≠ 0) :

(b + a) / b = 1 + a / b

theorem one_add_div {K : Type u} [division_ring K] {a b : K} (h : b ≠ 0) :

1 + a / b = (b + a) / b

theorem div_add_same {K : Type u} [division_ring K] {a b : K} (h : b ≠ 0) :

(a + b) / b = a / b + 1

theorem div_add_one {K : Type u} [division_ring K] {a b : K} (h : b ≠ 0) :

a / b + 1 = (a + b) / b

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

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

theorem same_sub_div {K : Type u} [division_ring K] {a b : K} (h : b ≠ 0) :

(b - a) / b = 1 - a / b

theorem one_sub_div {K : Type u} [division_ring K] {a b : K} (h : b ≠ 0) :

1 - a / b = (b - a) / b

theorem div_sub_same {K : Type u} [division_ring K] {a b : K} (h : b ≠ 0) :

(a - b) / b = a / b - 1

theorem div_sub_one {K : Type u} [division_ring K] {a b : K} (h : b ≠ 0) :

a / b - 1 = (a - b) / b

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

-a⁻¹ = (-a)⁻¹

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

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

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

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

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

a / -b = -(a / b)

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

(-a)⁻¹ = -a⁻¹

theorem one_div_mul_add_mul_one_div_eq_one_div_add_one_div {K : Type u} [division_ring K] {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} [division_ring K] {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} [division_ring K] (a b : K) {c : K} (hc : c ≠ 0) :

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

@[protected, instance]

def division_ring.is_domain {K : Type u} [division_ring K] :

@[instance]

def field.to_div_inv_monoid (K : Type u) [self : field K] :

div_inv_monoid 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 : K), a + b + c = a + (b + c)
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"
zsmul : ℤ → K → K
zsmul_zero' : (∀ (a : K), field.zsmul 0 a = 0) . "try_refl_tac"
zsmul_succ' : (∀ (n : ℕ) (a : K), field.zsmul (int.of_nat n.succ) a = a + field.zsmul (int.of_nat n) a) . "try_refl_tac"
zsmul_neg' : (∀ (n : ℕ) (a : K), field.zsmul -[1+ n] a = -field.zsmul ↑(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 : K), (a * b) * c = a * b * c
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 : K), a * (b + c) = a * b + a * c
right_distrib : ∀ (a b c : K), (a + b) * c = a * c + b * c
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"
zpow : ℤ → K → K
zpow_zero' : (∀ (a : K), field.zpow 0 a = 1) . "try_refl_tac"
zpow_succ' : (∀ (n : ℕ) (a : K), field.zpow (int.of_nat n.succ) a = a * field.zpow (int.of_nat n) a) . "try_refl_tac"
zpow_neg' : (∀ (n : ℕ) (a : K), field.zpow -[1+ n] a = (field.zpow ↑(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

@[protected, instance]

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

division_ring K

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 := _, zsmul := field.zsmul (show field K, from _inst_1), zsmul_zero' := _, zsmul_succ' := _, zsmul_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 := _, zpow := field.zpow (show field K, from _inst_1), zpow_zero' := _, zpow_succ' := _, zpow_neg' := _, exists_pair_ne := _, mul_inv_cancel := _, inv_zero := _}

@[protected, instance]

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

comm_group_with_zero K

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 := _, zpow := group_with_zero.zpow division_ring.to_group_with_zero, zpow_zero' := _, zpow_succ' := _, zpow_neg' := _, exists_pair_ne := _, inv_zero := _, mul_inv_cancel := _}

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.is_domain {K : Type u} [field K] :

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

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

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 := _, zsmul := ring.zsmul _inst_1, zsmul_zero' := _, zsmul_succ' := _, zsmul_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 := _, zpow := div_inv_monoid.zpow._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 _)), zpow_zero' := _, zpow_succ' := _, zpow_neg' := _, exists_pair_ne := _, mul_inv_cancel := _, inv_zero := _}

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] [division_ring K] (f : R →+* K) (u : units R) :

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

theorem ring_hom.map_ne_zero {K : Type u} {R : Type u_1} [division_ring K] [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} [division_ring K] [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] [division_ring K'] (g : K →+* K') (x : K) :

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

theorem ring_hom.map_div {K : Type u} {K' : Type u_2} [division_ring K] [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} [division_ring K] [semiring R] [nontrivial R] (f : K →+* R) :

function.injective ⇑f

noncomputable def division_ring_of_is_unit_or_eq_zero {R : Type u_1} [nontrivial R] [hR : ring R] (h : ∀ (a : R), is_unit a ∨ a = 0) :

division_ring R

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 := _, zsmul := ring.zsmul hR, zsmul_zero' := _, zsmul_succ' := _, zsmul_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 := _, zpow := group_with_zero.zpow (group_with_zero_of_is_unit_or_eq_zero h), zpow_zero' := _, zpow_succ' := _, zpow_neg' := _, exists_pair_ne := _, mul_inv_cancel := _, inv_zero := _}

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

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 := _, zsmul := comm_ring.zsmul hR, zsmul_zero' := _, zsmul_succ' := _, zsmul_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 := _, zpow := group_with_zero.zpow (group_with_zero_of_is_unit_or_eq_zero h), zpow_zero' := _, zpow_succ' := _, zpow_neg' := _, exists_pair_ne := _, mul_inv_cancel := _, inv_zero := _}

@[protected]

def function.injective.division_ring {K : Type u} [division_ring 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) :

division_ring K'

Pullback a division_ring along an injective function. See note [reducible non-instances].

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 := _, zsmul := ring.zsmul (function.injective.ring f hf zero one add mul neg sub), zsmul_zero' := _, zsmul_succ' := _, zsmul_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 := _, zpow := group_with_zero.zpow (function.injective.group_with_zero f hf zero one mul inv div), zpow_zero' := _, zpow_succ' := _, zpow_neg' := _, exists_pair_ne := _, mul_inv_cancel := _, inv_zero := _}

@[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. See note [reducible non-instances].

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 := _, zsmul := comm_ring.zsmul (function.injective.comm_ring f hf zero one add mul neg sub), zsmul_zero' := _, zsmul_succ' := _, zsmul_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 := _, zpow := comm_group_with_zero.zpow (function.injective.comm_group_with_zero f hf zero one mul inv div), zpow_zero' := _, zpow_succ' := _, zpow_neg' := _, exists_pair_ne := _, mul_inv_cancel := _, inv_zero := _}