instAddCommGroupWithOne — Mathlib

English

If α is AddGroupWithOne, then the matrix type M_n(α) admits an AddGroupWithOne structure, with integer casts realized by diagonal representations and compatible with addition.

Русский

Если α имеет AddGroupWithOne, то тип матриц M_n(α) получает структуру AddGroupWithOne; целочисленные приведения реализованы через диагональные представления и совместимы со сложением.

LaTeX

$$$M_n(\alpha) \text{ carries an } AddGroupWithOne \text{ with diagonal-based intCast.}$$$

Lean4

instance instAddCommGroupWithOne [AddCommGroupWithOne α] : AddCommGroupWithOne (Matrix n n α)
    where
  __ := addCommGroup
  __ := instAddGroupWithOne

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