instDivInvMonoid — Mathlib

English

The set of square matrices over a commutative ring carries a DivInvMonoid structure; i.e., it behaves like a division-inverse monoid under matrix operations.

Русский

Множество квадратных матриц над коммутативной кольцевой структурой образует структуру DivInvMonoid.

LaTeX

$$$$\mathrm{Mat}_{n'\times n'}(R) \text{ has a } \mathrm{DivInvMonoid} \text{ structure}.$$$$

Lean4

noncomputable instance : DivInvMonoid M :=
  { show Monoid M by infer_instance, show Inv M by infer_instance with }

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