instNonUnitalRing — Mathlib

English

If α is a nonunital ring, the set of n×n matrices over α forms a nonunital ring under the usual matrix operations.

Русский

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

LaTeX

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

Lean4

instance instNonUnitalRing [Fintype n] [NonUnitalRing α] : NonUnitalRing (Matrix n n α) :=
  { Matrix.nonUnitalSemiring, Matrix.addCommGroup with }

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