toIsField — Mathlib

English

If R is a field, then R satisfies the IsField axioms; in particular, existence and behavior of inverses follow from field axioms.

Русский

Если R — поле, то R удовлетворяет аксиомам IsField; в частности существуют обратные элементы и задаются их свойства.

LaTeX

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

Lean4

/-- Transferring from `Field` to `IsField`. -/
theorem toIsField (R : Type u) [Field R] : IsField R :=
  Semifield.toIsField _

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