instNonAssocRing — Mathlib

English

If α is a nonassociative ring and n is finite with a decidable equality on n, then the matrix ring M_n(α) is a nonassociative ring.

Русский

Если α — неассоциативное кольцо, и n конечное с разрешимым равенством на n, тогда M_n(α) образует неассоциативное кольцо.

LaTeX

$$$\\mathrm{NonAssocRing}\\big(\\mathrm{Matrix}_n(\\alpha)\\big)$$$

Lean4

instance instNonAssocRing [Fintype n] [DecidableEq n] [NonAssocRing α] : NonAssocRing (Matrix n n α) :=
  { Matrix.nonAssocSemiring, Matrix.instAddCommGroupWithOne with }

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