mathlib3 documentation

algebra.field.defs

Division (semi)rings and (semi)fields #

THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.

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_semiring: Nontrivial semiring with multiplicative inverses for nonzero elements.
division_ring: : Nontrivial ring with multiplicative inverses for nonzero elements.
semifield: Commutative division semiring.
field: Commutative division ring.
is_field: Predicate on a (semi)ring that it is a (semi)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

def rat.cast_rec {K : Type u_3} [has_lift_t ℕ K] [has_lift_t ℤ K] [has_mul K] [has_inv K] :

The default definition of the coercion (↑(a : ℚ) : K) for a division ring K is defined as (a / b : K) = (a : K) * (b : K)⁻¹. Use coe instead of rat.cast_rec for better definitional behaviour.

Equations

{num := a, denom := b, pos := _x, cop := _x_1}.cast_rec = ↑a * (↑b)⁻¹

@[class]

structure has_rat_cast (K : Type u) :

rat_cast : ℚ → K

Type class for the canonical homomorphism ℚ → K.

Instances of this typeclass

Instances of other typeclasses for has_rat_cast

has_rat_cast.has_sizeof_inst

def qsmul_rec {K : Type u_3} (coe : ℚ → K) [has_mul K] (a : ℚ) (x : K) :

K

The default definition of the scalar multiplication (a : ℚ) • (x : K) for a division ring K is given by a • x = (↑ a) * x. Use (a : ℚ) • (x : K) instead of qsmul_rec for better definitional behaviour.

Equations

qsmul_rec coe a x = coe a * x

@[class]

structure division_semiring (α : Type u_4) :

Type u_4

add : α → α → α
add_assoc : ∀ (a b c : α), a + b + c = a + (b + c)
zero : α
zero_add : ∀ (a : α), 0 + a = a
add_zero : ∀ (a : α), a + 0 = a
nsmul : ℕ → α → α
nsmul_zero' : (∀ (x : α), division_semiring.nsmul 0 x = 0) . "try_refl_tac"
nsmul_succ' : (∀ (n : ℕ) (x : α), division_semiring.nsmul n.succ x = x + division_semiring.nsmul n x) . "try_refl_tac"
add_comm : ∀ (a b : α), a + b = b + a
mul : α → α → α
left_distrib : ∀ (a b c : α), a * (b + c) = a * b + a * c
right_distrib : ∀ (a b c : α), (a + b) * c = a * c + b * c
zero_mul : ∀ (a : α), 0 * a = 0
mul_zero : ∀ (a : α), a * 0 = 0
mul_assoc : ∀ (a b c : α), a * b * c = a * (b * c)
one : α
one_mul : ∀ (a : α), 1 * a = a
mul_one : ∀ (a : α), a * 1 = a
nat_cast : ℕ → α
nat_cast_zero : division_semiring.nat_cast 0 = 0 . "control_laws_tac"
nat_cast_succ : (∀ (n : ℕ), division_semiring.nat_cast (n + 1) = division_semiring.nat_cast n + 1) . "control_laws_tac"
npow : ℕ → α → α
npow_zero' : (∀ (x : α), division_semiring.npow 0 x = 1) . "try_refl_tac"
npow_succ' : (∀ (n : ℕ) (x : α), division_semiring.npow n.succ x = x * division_semiring.npow n x) . "try_refl_tac"
inv : α → α
div : α → α → α
div_eq_mul_inv : (∀ (a b : α), a / b = a * b⁻¹) . "try_refl_tac"
zpow : ℤ → α → α
zpow_zero' : (∀ (a : α), division_semiring.zpow 0 a = 1) . "try_refl_tac"
zpow_succ' : (∀ (n : ℕ) (a : α), division_semiring.zpow (int.of_nat n.succ) a = a * division_semiring.zpow (int.of_nat n) a) . "try_refl_tac"
zpow_neg' : (∀ (n : ℕ) (a : α), division_semiring.zpow -[1+ n] a = (division_semiring.zpow ↑(n.succ) a)⁻¹) . "try_refl_tac"
exists_pair_ne : ∃ (x y : α), x ≠ y
inv_zero : 0⁻¹ = 0
mul_inv_cancel : ∀ (a : α), a ≠ 0 → a * a⁻¹ = 1

A division_semiring is a semiring with multiplicative inverses for nonzero elements.

Instances of this typeclass

Instances of other typeclasses for division_semiring

division_semiring.has_sizeof_inst

@[instance]

def division_semiring.to_group_with_zero (α : Type u_4) [self : division_semiring α] :

group_with_zero α

@[instance]

def division_semiring.to_semiring (α : Type u_4) [self : division_semiring α] :

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

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
int_cast : ℤ → K
nat_cast : ℕ → K
one : K
nat_cast_zero : division_ring.nat_cast 0 = 0 . "control_laws_tac"
nat_cast_succ : (∀ (n : ℕ), division_ring.nat_cast (n + 1) = division_ring.nat_cast n + 1) . "control_laws_tac"
int_cast_of_nat : (∀ (n : ℕ), division_ring.int_cast ↑n = ↑n) . "control_laws_tac"
int_cast_neg_succ_of_nat : (∀ (n : ℕ), division_ring.int_cast (-↑(n + 1)) = -↑(n + 1)) . "control_laws_tac"
mul : K → K → K
mul_assoc : ∀ (a b c : K), a * b * c = a * (b * c)
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
rat_cast : ℚ → K
mul_inv_cancel : ∀ {a : K}, a ≠ 0 → a * a⁻¹ = 1
inv_zero : 0⁻¹ = 0
rat_cast_mk : (∀ (a : ℤ) (b : ℕ) (h1 : 0 < b) (h2 : a.nat_abs.coprime b), division_ring.rat_cast {num := a, denom := b, pos := h1, cop := h2} = ↑a * (↑b)⁻¹) . "try_refl_tac"
qsmul : ℚ → K → K
qsmul_eq_mul' : (∀ (a : ℚ) (x : K), division_ring.qsmul a x = division_ring.rat_cast a * x) . "try_refl_tac"

A division_ring is a ring with multiplicative inverses for nonzero elements.

An instance of division_ring K includes maps rat_cast : ℚ → K and qsmul : ℚ → K → K. If the division ring has positive characteristic p, we define rat_cast (1 / p) = 1 / 0 = 0 for consistency with our division by zero convention. The fields rat_cast and qsmul are needed to implement the algebra_rat [division_ring K] : algebra ℚ K instance, since we need to control the specific definitions for some special cases of K (in particular K = ℚ itself). See also Note [forgetful inheritance].

Instances of this typeclass

Instances of other typeclasses for division_ring

division_ring.has_sizeof_inst

@[instance]

def division_ring.to_ring (K : Type u) [self : division_ring K] :

@[instance]

def division_ring.to_has_rat_cast (K : Type u) [self : division_ring K] :

@[protected, instance]

def division_ring.to_division_semiring {α : Type u_1} [division_ring α] :

division_semiring α

Equations

division_ring.to_division_semiring = {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' := _, add_comm := _, mul := division_ring.mul _inst_1, left_distrib := _, right_distrib := _, zero_mul := _, mul_zero := _, mul_assoc := _, one := division_ring.one _inst_1, one_mul := _, mul_one := _, nat_cast := division_ring.nat_cast _inst_1, nat_cast_zero := _, nat_cast_succ := _, npow := division_ring.npow _inst_1, npow_zero' := _, npow_succ' := _, 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 := _}

@[instance]

def semifield.to_comm_semiring (α : Type u_4) [self : semifield α] :

comm_semiring α

@[instance]

def semifield.to_comm_group_with_zero (α : Type u_4) [self : semifield α] :

comm_group_with_zero α

@[instance]

def semifield.to_division_semiring (α : Type u_4) [self : semifield α] :

division_semiring α

@[class]

structure semifield (α : Type u_4) :

Type u_4

add : α → α → α
add_assoc : ∀ (a b c : α), a + b + c = a + (b + c)
zero : α
zero_add : ∀ (a : α), 0 + a = a
add_zero : ∀ (a : α), a + 0 = a
nsmul : ℕ → α → α
nsmul_zero' : (∀ (x : α), semifield.nsmul 0 x = 0) . "try_refl_tac"
nsmul_succ' : (∀ (n : ℕ) (x : α), semifield.nsmul n.succ x = x + semifield.nsmul n x) . "try_refl_tac"
add_comm : ∀ (a b : α), a + b = b + a
mul : α → α → α
left_distrib : ∀ (a b c : α), a * (b + c) = a * b + a * c
right_distrib : ∀ (a b c : α), (a + b) * c = a * c + b * c
zero_mul : ∀ (a : α), 0 * a = 0
mul_zero : ∀ (a : α), a * 0 = 0
mul_assoc : ∀ (a b c : α), a * b * c = a * (b * c)
one : α
one_mul : ∀ (a : α), 1 * a = a
mul_one : ∀ (a : α), a * 1 = a
nat_cast : ℕ → α
nat_cast_zero : semifield.nat_cast 0 = 0 . "control_laws_tac"
nat_cast_succ : (∀ (n : ℕ), semifield.nat_cast (n + 1) = semifield.nat_cast n + 1) . "control_laws_tac"
npow : ℕ → α → α
npow_zero' : (∀ (x : α), semifield.npow 0 x = 1) . "try_refl_tac"
npow_succ' : (∀ (n : ℕ) (x : α), semifield.npow n.succ x = x * semifield.npow n x) . "try_refl_tac"
mul_comm : ∀ (a b : α), a * b = b * a
inv : α → α
div : α → α → α
div_eq_mul_inv : (∀ (a b : α), a / b = a * b⁻¹) . "try_refl_tac"
zpow : ℤ → α → α
zpow_zero' : (∀ (a : α), semifield.zpow 0 a = 1) . "try_refl_tac"
zpow_succ' : (∀ (n : ℕ) (a : α), semifield.zpow (int.of_nat n.succ) a = a * semifield.zpow (int.of_nat n) a) . "try_refl_tac"
zpow_neg' : (∀ (n : ℕ) (a : α), semifield.zpow -[1+ n] a = (semifield.zpow ↑(n.succ) a)⁻¹) . "try_refl_tac"
exists_pair_ne : ∃ (x y : α), x ≠ y
inv_zero : 0⁻¹ = 0
mul_inv_cancel : ∀ (a : α), a ≠ 0 → a * a⁻¹ = 1

A semifield is a comm_semiring with multiplicative inverses for nonzero elements.

Instances of this typeclass

Instances of other typeclasses for semifield

semifield.has_sizeof_inst

@[instance]

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

@[instance]

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

division_ring K

@[class]

structure field (K : 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
int_cast : ℤ → K
nat_cast : ℕ → K
one : K
nat_cast_zero : field.nat_cast 0 = 0 . "control_laws_tac"
nat_cast_succ : (∀ (n : ℕ), field.nat_cast (n + 1) = field.nat_cast n + 1) . "control_laws_tac"
int_cast_of_nat : (∀ (n : ℕ), field.int_cast ↑n = ↑n) . "control_laws_tac"
int_cast_neg_succ_of_nat : (∀ (n : ℕ), field.int_cast (-↑(n + 1)) = -↑(n + 1)) . "control_laws_tac"
mul : K → K → K
mul_assoc : ∀ (a b c : K), a * b * c = a * (b * c)
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
rat_cast : ℚ → K
mul_inv_cancel : ∀ {a : K}, a ≠ 0 → a * a⁻¹ = 1
inv_zero : 0⁻¹ = 0
rat_cast_mk : (∀ (a : ℤ) (b : ℕ) (h1 : 0 < b) (h2 : a.nat_abs.coprime b), field.rat_cast {num := a, denom := b, pos := h1, cop := h2} = ↑a * (↑b)⁻¹) . "try_refl_tac"
qsmul : ℚ → K → K
qsmul_eq_mul' : (∀ (a : ℚ) (x : K), field.qsmul a x = field.rat_cast a * x) . "try_refl_tac"

A field is a comm_ring with multiplicative inverses for nonzero elements.

An instance of field K includes maps of_rat : ℚ → K and qsmul : ℚ → K → K. If the field has positive characteristic p, we define of_rat (1 / p) = 1 / 0 = 0 for consistency with our division by zero convention. The fields of_rat and qsmul are needed to implement thealgebra_rat [division_ring K] : algebra ℚ Kinstance, since we need to control the specific definitions for some special cases ofK(in particularK = ℚ` itself). See also Note [forgetful inheritance].

Instances of this typeclass

Instances of other typeclasses for field

field.has_sizeof_inst

@[protected, instance]

def rat.cast_coe {K : Type u_1} [has_rat_cast K] :

has_coe_t ℚ K

Construct the canonical injection from ℚ into an arbitrary division ring. If the field has positive characteristic p, we define 1 / p = 1 / 0 = 0 for consistency with our division by zero convention.

Equations

rat.cast_coe = {coe := has_rat_cast.rat_cast _inst_2}

theorem rat.cast_mk' {K : Type u_3} [division_ring K] (a : ℤ) (b : ℕ) (h1 : 0 < b) (h2 : a.nat_abs.coprime b) :

↑{num := a, denom := b, pos := h1, cop := h2} = ↑a * (↑b)⁻¹

theorem rat.cast_def {K : Type u_3} [division_ring K] (r : ℚ) :

↑r = ↑(r.num) / ↑(r.denom)

@[protected, instance]

def rat.smul_division_ring {K : Type u_3} [division_ring K] :

Equations

rat.smul_division_ring = {smul := division_ring.qsmul _inst_1}

theorem rat.smul_def {K : Type u_3} [division_ring K] (a : ℚ) (x : K) :

a • x = ↑a * x

@[simp]

theorem rat.smul_one_eq_coe (A : Type u_1) [division_ring A] (m : ℚ) :

m • 1 = ↑m

@[protected, instance]

def field.to_semifield {K : Type u_3} [field K] :

Equations

field.to_semifield = {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' := _, add_comm := _, mul := field.mul _inst_1, left_distrib := _, right_distrib := _, zero_mul := _, mul_zero := _, mul_assoc := _, one := field.one _inst_1, one_mul := _, mul_one := _, nat_cast := field.nat_cast _inst_1, nat_cast_zero := _, nat_cast_succ := _, npow := field.npow _inst_1, npow_zero' := _, npow_succ' := _, mul_comm := _, inv := field.inv _inst_1, div := field.div _inst_1, div_eq_mul_inv := _, zpow := field.zpow _inst_1, zpow_zero' := _, zpow_succ' := _, zpow_neg' := _, exists_pair_ne := _, inv_zero := _, mul_inv_cancel := _}

structure is_field (R : Type u) [semiring 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 (semi)ring is a (semi)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 (semi)field.

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

Transferring from semifield to is_field.

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

Transferring from field to is_field.

@[simp]

theorem is_field.nontrivial {R : Type u} [semiring R] (h : is_field R) :

@[simp]

theorem not_is_field_of_subsingleton (R : Type u) [semiring R] [subsingleton R] :

noncomputable def is_field.to_semifield {R : Type u} [semiring R] (h : is_field R) :

Transferring from is_field to semifield.

Equations

h.to_semifield = {add := semiring.add _inst_1, add_assoc := _, zero := semiring.zero _inst_1, zero_add := _, add_zero := _, nsmul := semiring.nsmul _inst_1, nsmul_zero' := _, nsmul_succ' := _, add_comm := _, mul := semiring.mul _inst_1, left_distrib := _, right_distrib := _, zero_mul := _, mul_zero := _, mul_assoc := _, one := semiring.one _inst_1, one_mul := _, mul_one := _, nat_cast := semiring.nat_cast _inst_1, nat_cast_zero := _, nat_cast_succ := _, npow := semiring.npow _inst_1, npow_zero' := _, npow_succ' := _, mul_comm := _, inv := λ (a : R), dite (a = 0) (λ (ha : a = 0), 0) (λ (ha : ¬a = 0), classical.some _), div := division_semiring.div._default semiring.mul semiring.mul_assoc semiring.one semiring.one_mul semiring.mul_one semiring.npow semiring.npow_zero' semiring.npow_succ' (λ (a : R), dite (a = 0) (λ (ha : a = 0), 0) (λ (ha : ¬a = 0), classical.some _)), div_eq_mul_inv := _, zpow := division_semiring.zpow._default semiring.mul semiring.mul_assoc semiring.one semiring.one_mul semiring.mul_one semiring.npow semiring.npow_zero' semiring.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 := _, inv_zero := _, mul_inv_cancel := _}

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

Transferring from is_field to field.

Equations

h.to_field = {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 := _, int_cast := ring.int_cast _inst_1, nat_cast := ring.nat_cast _inst_1, one := ring.one _inst_1, nat_cast_zero := _, nat_cast_succ := _, int_cast_of_nat := _, int_cast_neg_succ_of_nat := _, mul := ring.mul _inst_1, mul_assoc := _, one_mul := _, mul_one := _, npow := ring.npow _inst_1, npow_zero' := _, npow_succ' := _, left_distrib := _, right_distrib := _, mul_comm := _, inv := semifield.inv h.to_semifield, div := semifield.div h.to_semifield, div_eq_mul_inv := _, zpow := semifield.zpow h.to_semifield, zpow_zero' := _, zpow_succ' := _, zpow_neg' := _, exists_pair_ne := _, rat_cast := division_ring.rat_cast._default ring.add ring.add_assoc ring.zero ring.zero_add ring.add_zero ring.nsmul ring.nsmul_zero' ring.nsmul_succ' ring.neg ring.sub ring.sub_eq_add_neg ring.zsmul ring.zsmul_zero' ring.zsmul_succ' ring.zsmul_neg' ring.add_left_neg ring.add_comm ring.int_cast ring.nat_cast ring.one ring.nat_cast_zero ring.nat_cast_succ ring.int_cast_of_nat ring.int_cast_neg_succ_of_nat ring.mul ring.mul_assoc ring.one_mul ring.mul_one ring.npow ring.npow_zero' ring.npow_succ' ring.left_distrib ring.right_distrib semifield.inv semifield.div _ semifield.zpow _ _ _, mul_inv_cancel := _, inv_zero := _, rat_cast_mk := _, qsmul := division_ring.qsmul._default (… ring.zsmul_zero' ring.zsmul_succ' ring.zsmul_neg' ring.add_left_neg ring.add_comm ring.int_cast ring.nat_cast ring.one ring.nat_cast_zero ring.nat_cast_succ ring.int_cast_of_nat ring.int_cast_neg_succ_of_nat ring.mul ring.mul_assoc ring.one_mul ring.mul_one ring.npow ring.npow_zero' ring.npow_succ' ring.left_distrib ring.right_distrib semifield.inv semifield.div _ semifield.zpow _ _ _) ring.add ring.add_assoc ring.zero ring.zero_add ring.add_zero ring.nsmul ring.nsmul_zero' ring.nsmul_succ' ring.neg ring.sub ring.sub_eq_add_neg ring.zsmul ring.zsmul_zero' ring.zsmul_succ' ring.zsmul_neg' ring.add_left_neg ring.add_comm ring.int_cast ring.nat_cast ring.one ring.nat_cast_zero ring.nat_cast_succ ring.int_cast_of_nat ring.int_cast_neg_succ_of_nat ring.mul ring.mul_assoc ring.one_mul ring.mul_one ring.npow ring.npow_zero' ring.npow_succ' ring.left_distrib ring.right_distrib, qsmul_eq_mul' := _}

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.