commRing — Mathlib

English

There is a commutative ring structure on ℤ√d (alternative presentation via inference).

Русский

Существует коммутативная кольцевая структура на ℤ√d (альтернативная формулировка через вывод).

LaTeX

$$$\\mathbb{Z}[\\sqrt{d}] \\text{ is a commutative ring.}$$$

Lean4

instance commRing : CommRing (ℤ√d) := by
  refine
            { Zsqrtd.addGroupWithOne with
              mul := (· * ·)
              npow := @npowRec (ℤ√d) ⟨1⟩ ⟨(· * ·)⟩, add_comm := ?_
              left_distrib := ?_
              right_distrib := ?_
              zero_mul := ?_
              mul_zero := ?_
              mul_assoc := ?_
              one_mul := ?_
              mul_one := ?_
              mul_comm := ?_ } <;>
          intros <;>
        ext <;>
      simp <;>
    ring

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