instCommRing — Mathlib

English

X_q is a commutative ring; in particular multiplication is commutative: (a,b)·(c,d) = (c,d)·(a,b).

Русский

X_q является коммутативным кольцом; в частности умножение коммутативно: (a,b)·(c,d) = (c,d)·(a,b).

LaTeX

$$$X_q \text{ is a commutative ring with the above operations; } (a,b)\cdot(c,d)=(ac+3bd, ad+bc) = (c,d)\cdot(a,b).$$$

Lean4

instance : CommRing (X q) :=
  { inferInstanceAs (Ring (X q)) with mul_comm := fun _ _ ↦ by ext <;> dsimp <;> ring }

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