commRing — Mathlib

English

ℚ is a commutative ring.

Русский

Кольцо рациональных чисел ℚ коммутативно как кольцо.

LaTeX

$$$ \\mathbb{Q} \\text{ is a CommRing}. $$$

Lean4

instance commRing : CommRing ℚ where
  __ := addCommGroup
  __ := commMonoid
  zero_mul := Rat.zero_mul
  mul_zero := Rat.mul_zero
  left_distrib := Rat.mul_add
  right_distrib := Rat.add_mul
  intCast := fun n => n
  natCast n := Int.cast n
  natCast_zero := rfl
  natCast_succ
    n := by
    simp only [intCast_eq_divInt, divInt_add_divInt _ _ Int.one_ne_zero Int.one_ne_zero, ← divInt_one_one,
      Int.natCast_add, Int.natCast_one, mul_one]

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