toIsField — Mathlib

English

If R is a semifield, then R is a field; i.e., every nonzero element has a multiplicative inverse.

Русский

Если R является семифилдом, то R является полем; то есть для каждого ненулевого элемента существует обратный по умножению.

LaTeX

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

Lean4

/-- Transferring from `Semifield` to `IsField`. -/
theorem toIsField (R : Type u) [Semifield R] : IsField R
    where
  __ := ‹Semifield R›
  mul_inv_cancel {a} ha := ⟨a⁻¹, mul_inv_cancel₀ ha⟩

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