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.

structure IsField (R : Type u) [Semiring R] :
  • exists_pair_ne : x y, 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 0b, a * b = 1

    Nonzero elements have multiplicative inverses.

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.

Instances For
    theorem Semifield.toIsField (R : Type u) [Semifield R] :

    Transferring from Semifield to IsField.

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

    Transferring from Field to IsField.

    theorem IsField.nontrivial {R : Type u} [Semiring R] (h : IsField R) :
    noncomputable def IsField.toSemifield {R : Type u} [Semiring R] (h : IsField R) :

    Transferring from IsField to Semifield.

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

      Transferring from IsField to Field.

      Instances For
        theorem uniq_inv_of_isField (R : Type u) [Ring R] (hf : IsField R) (x : R) :
        x 0∃! y, 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.