instRing — Mathlib

English

If α is a ring, then the set of n×n matrices over α forms a ring under the usual addition and multiplication.

Русский

Если α — кольцо, тогда множество матриц размерa n×n над α образует кольцо под обычными операциями сложения и умножения.

LaTeX

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

Lean4

instance instRing [Fintype n] [DecidableEq n] [Ring α] : Ring (Matrix n n α) :=
  { Matrix.semiring, Matrix.instAddCommGroupWithOne with }

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