English
Left multiplication by a fixed matrix M defines an additive monoid homomorphism from Matrix m n α to Matrix l n α; i.e., X ↦ M X preserves addition and zero: M X + M Y = M (X + Y) and M 0 = 0.
Русский
Левое умножение фиксированной матрицей M задаёт гомоморфизм прибавления от Matrix m n α к Matrix l n α; то есть MX + MY = M(X+Y) и M0 = 0.
LaTeX
$$$ M X + M Y = M(X+Y) \\quad \\text{и} \\quad M 0 = 0 $$$
Lean4
/-- Left multiplication by a matrix, as an `AddMonoidHom` from matrices to matrices. -/
@[simps]
def addMonoidHomMulLeft [Fintype m] (M : Matrix l m α) : Matrix m n α →+ Matrix l n α
where
toFun x := M * x
map_zero' := Matrix.mul_zero _
map_add' := Matrix.mul_add _
