English
If α has an AddMonoidWithOne structure, then the set of n×n matrices over α, M_n(α), carries an AddMonoidWithOne structure, with diag providing the natCast embedding: natCast 0 = diag 0 and natCast (succ n) = diag n + diag 1.
Русский
Пусть α имеет структуру AddMonoidWithOne. Тогда множество квадратных матриц M_n(α) имеет структуру AddMonoidWithOne; вложение натуральных чисел в матрицы задаётся как diag(n), и natCast удовлетворяет natCast 0 = diag 0 и natCast (succ n) = diag n + diag 1.
LaTeX
$$$M_n(\alpha) \text{ является } AddMonoidWithOne \text{, natCast(k) определяется как } \mathrm{diag}(k).$$$
Lean4
instance instAddMonoidWithOne [AddMonoidWithOne α] : AddMonoidWithOne (Matrix n n α)
where
natCast_zero := show diagonal _ = _ by rw [Nat.cast_zero, diagonal_zero]
natCast_succ n := show diagonal _ = diagonal _ + _ by rw [Nat.cast_succ, ← diagonal_add, diagonal_one]
