toSemifield — Mathlib

English

From IsField on R, one obtains a semifield structure on R.

Русский

Из IsField на R получается структура семифилда на R.

LaTeX

$$$IsField\,R \Rightarrow Semifield\,R$$$

Lean4

/-- Transferring from `IsField` to `Semifield`. -/
noncomputable def toSemifield {R : Type u} [Semiring R] (h : IsField R) : Semifield R
    where
  __ := ‹Semiring R›
  __ := h
  inv a := if ha : a = 0 then 0 else Classical.choose (h.mul_inv_cancel ha)
  inv_zero := dif_pos rfl
  mul_inv_cancel a ha := by convert Classical.choose_spec (h.mul_inv_cancel ha); exact dif_neg ha
  nnqsmul := _
  nnqsmul_def _ _ := rfl

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