addMonoidHomMulRight — Mathlib

English

Right multiplication by a fixed matrix M defines an additive monoid homomorphism from Matrix l m α to Matrix l n α; i.e., X ↦ X M preserves addition and zero: (X + Y) M = X M + Y M and 0 M = 0.

Русский

Правое умножение фиксированной матрицей M задаёт аддитивный гомоморфизм: (X+Y)M = XM + YM и 0·M = 0.

LaTeX

$$$ (X + Y) M = X M + Y M \\quad \\text{и} \\quad 0 M = 0 $$$

Lean4

/-- Right multiplication by a matrix, as an `AddMonoidHom` from matrices to matrices. -/
@[simps]
def addMonoidHomMulRight [Fintype m] (M : Matrix m n α) : Matrix l m α →+ Matrix l n α
    where
  toFun x := x * M
  map_zero' := Matrix.zero_mul _
  map_add' _ _ := Matrix.add_mul _ _ _

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