monoid — Mathlib

English

The set SL(n, R) forms a monoid (indeed a group) under matrix multiplication, with the identity given by the identity matrix.

Русский

Множество SL(n, R) образует моноид (и группу) под умножением матриц; единица — это единичная матрица.

LaTeX

$$SL_n(R) is a monoid (indeed a group) under matrix multiplication with identity I_n$$

Lean4

instance monoid : Monoid (SpecialLinearGroup n R) :=
  Function.Injective.monoid _ Subtype.coe_injective coe_one coe_mul coe_pow

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