instField — Mathlib

English

The rational numbers form a field.

Русский

Рациональные числа образуют поле.

LaTeX

$$$\mathbb{Q} \text{ is a field}$$$

Lean4

instance instField : Field ℚ where
  __ := commRing
  __ := commGroupWithZero
  nnqsmul := _
  nnqsmul_def := fun _ _ => rfl
  qsmul := _
  qsmul_def := fun _ _ => rfl
  nnratCast_def q := by rw [← NNRat.den_coe, ← Int.cast_natCast q.num, ← NNRat.num_coe]; exact (num_div_den _).symm
  ratCast_def _ := (num_div_den _).symm

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