# `IsField` predicate #

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.

source
structure IsField (R : Type u) [Semiring R] :
Prop

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. Additionally, this is useful when trying to prove that a particular ring structure extends to a (semi)field.

- exists_pair_ne : ∃ (x : R), ∃ (y : R), x ≠ y

  For a semiring to be a field, it must have two distinct elements.

- mul_comm (x y : R) : x * y = y * x

  Fields are commutative.

- mul_inv_cancel {a : R} : a ≠ 0 → ∃ (b : R), a * b = 1

  Nonzero elements have multiplicative inverses.

Instances For

source
theorem Semifield.toIsField (R : Type u) [Semifield R] :
IsField R

Transferring from `Semifield` to `IsField`.

source
theorem Field.toIsField (R : Type u) [Field R] :
IsField R

Transferring from `Field` to `IsField`.

source
@[simp]
theorem IsField.nontrivial {R : Type u} [Semiring R] (h : IsField R) :
Nontrivial R
source
theorem IsField.isDomain {R : Type u} [Semiring R] (h : IsField R) :
IsDomain R
source
instance instIsDomain {R : Type u} [Semifield R] :
IsDomain R
source
@[simp]
theorem not_isField_of_subsingleton (R : Type u) [Semiring R] [Subsingleton R] :
¬IsField R
source
noncomputable def IsField.toSemifield {R : Type u} [Semiring R] (h : IsField R) :
Semifield R

Transferring from `IsField` to `Semifield`.

Equations

- One or more equations did not get rendered due to their size.

Instances For

source
noncomputable def IsField.toField {R : Type u} [Ring R] (h : IsField R) :
Field R

Transferring from `IsField` to `Field`.

Equations

- One or more equations did not get rendered due to their size.

Instances For

source
theorem uniq_inv_of_isField (R : Type u) [Ring R] (hf : IsField 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 `IsField` doesn't remember the data of an `inv` function and as such, a lemma that there is a unique inverse could be useful.