instField — Mathlib

English

The nimber type carries a field structure: with addition and multiplication, every nonzero nimber has a multiplicative inverse, and the usual field axioms (associativity, commutativity, distributivity, etc.) hold.

Русский

Тип Nimber обладает структурой поля: при сложении и умножении каждый ненулевой Nimber имеет обратный по умножению, выполняются обычные аксиомы поля (ассоциативность, коммутативность, дистрибутивность и пр.).

LaTeX

$$$\mathrm{Field}(\mathrm{Nimber})$$$

Lean4

instance : Field Nimber
    where
  mul_inv_cancel a ha := by rw [inv_eq_invAux ha, mul_invAux_cancel ha]
  inv_zero := dif_pos rfl
  nnqsmul := _
  qsmul := _

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