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

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

Transferring from Semifield to IsField.

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

Transferring from Field to IsField.

@[simp]

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

@[simp]

theorem not_isField_of_subsingleton (R : Type u) [Semiring R] [Subsingleton R] : ¬IsField R

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

Transferring from IsField to Semifield.

Equations

• IsField.toSemifield h = let __spread.0 := inst; let __spread.1 := h; Semifield.mk ⋯ zpowRec ⋯ ⋯ ⋯ ⋯ ⋯ ⋯ (fun (q : ℚ≥0) (a : R) => ↑q * a) ⋯

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

Transferring from IsField to Field.

Equations

• IsField.toField h = let __src := inst; let __src_1 := IsField.toSemifield h; Field.mk ⋯ Semifield.zpow ⋯ ⋯ ⋯ ⋯ ⋯ ⋯ Semifield.nnqsmul ⋯ ⋯ (fun (a : ℚ) (x : R) => ↑a * x) ⋯

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.