`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.

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.

Fields are commutative.

Nonzero elements have multiplicative inverses.

## Instances For

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.