English
For fixed i, j, the map a ↦ single i j a is an additive monoid hom α →+ Matrix m n α, with toFun = single i j a and preserving zero and addition.
Русский
Для фиксированных i, j отображение a ↦ single i j a является аддитивным одомом α →+ Matrix m n α, т.е. toFun = single i j a и сохраняет нуль и сложение.
LaTeX
$$$ \\text{singleAddMonoidHom } i j : α \\to+ Matrix m n α \\\\ \\text{toFun} = \\mathrm{single}_{i j}, \\; \\mathrm{map\\_zero}' = \\mathrm{single\\_zero}, \\; \\mathrm{map\\_add}'(a,b) = \\mathrm{single}_{i j} a + \\mathrm{single}_{i j} b. $$$
Lean4
/-- `Matrix.single` as a bundled additive map. -/
@[simps]
def singleAddMonoidHom [AddCommMonoid α] (i : m) (j : n) : α →+ Matrix m n α
where
toFun := single i j
map_zero' := single_zero _ _
map_add' _ _ := single_add _ _ _ _
