toField — Mathlib

English

From IsField on a ring, one can equip the same set with a Field structure.

Русский

На том же множество можно снабдить структурой поля, если дано IsField.

LaTeX

$$$IsField\,R \Rightarrow Field\,R$$$

Lean4

/-- Transferring from `IsField` to `Field`. -/
noncomputable def toField {R : Type u} [Ring R] (h : IsField R) : Field R
    where
  __ :=
    (‹Ring R› :) -- this also works without the `( :)`, but it's slow

  __ := h.toSemifield
  qsmul := _
  qsmul_def := fun _ _ => rfl

Похожие утверждения