instField — Mathlib

English

If β is a field, then Germ β carries a field structure; both addition and multiplication, and inverses, are defined termwise on representatives.

Русский

Если β — поле, то Germ β обладает структурой поля; операции сложения, умножения и обратные элементы определяются по представителям.

LaTeX

$$$\\text{β}^* \\text{ имеет структуру поля, если } β \\text{ — поле}$$$

Lean4

instance instField [Field β] : Field β* where
  __ := instCommRing
  __ := instDivisionRing

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