English
If α has an AddGroupWithOne structure, then M_n(α) inherits an AddGroupWithOne structure extending the existing AddGroupWithOne and AddMonoidWithOne structures; the intCast and natCast are compatible with diagonal representations.
Русский
Пусть α обладает структурой AddGroupWithOne. Тогда M_n(α) наследует структуру AddGroupWithOne, продолжающую существующую AddGroupWithOne и AddMonoidWithOne; целочисленные и натуральные преобразования согласованы с диагональными представлениями.
LaTeX
$$$M_n(\alpha) \text{ имеет } AddGroupWithOne, совместимую с диагональным отображением. $$$
Lean4
instance instAddGroupWithOne [AddGroupWithOne α] : AddGroupWithOne (Matrix n n α)
where
intCast_ofNat n := show diagonal _ = diagonal _ by rw [Int.cast_natCast]
intCast_negSucc n := show diagonal _ = -(diagonal _) by rw [Int.cast_negSucc, diagonal_neg]
__ := addGroup
__ := instAddMonoidWithOne
