instRing — Mathlib

English

X_q forms a ring with the above addition and multiplication: the usual ring axioms hold (distributivity, zero and one, etc.).

Русский

X_q образует кольцо с вышеуказанными операциями сложения и умножения: выполняются стандартные аксиомы кольца.

LaTeX

$$$X_q \text{ is a ring with } (a,b)+(c,d)=(a+c,b+d),\ (a,b)\cdot(c,d)=(ac+3bd, ad+bc),\ 0=(0,0),\ 1=(1,0).$$$

Lean4

instance : Ring (X q) :=
  { inferInstanceAs (AddGroupWithOne (X q)), inferInstanceAs (AddCommGroup (X q)),
    inferInstanceAs (Monoid (X q)) with
    left_distrib := left_distrib
    right_distrib := right_distrib
    mul_zero := fun _ ↦ by ext <;> simp
    zero_mul := fun _ ↦ by ext <;> simp }

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