instField — Mathlib

English

If p is prime, then ZMod p carries a field structure (the integers modulo p form a field).

Русский

Если p простое, то ZMod p — это поле (целые числа по модулю p образуют поле).

LaTeX

$$If p is prime, then ZMod p is a field.$$

Lean4

/-- Field structure on `ZMod p` if `p` is prime. -/
instance : Field (ZMod p) where
  mul_inv_cancel := mul_inv_cancel_aux p
  inv_zero := inv_zero p
  nnqsmul := _
  nnqsmul_def := fun _ _ => rfl
  qsmul := _
  qsmul_def := fun _ _ => rfl

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