singleLinearMap — Mathlib

English

For fixed i, j, the map a ↦ single i j a is a linear map α →ₗ[R] Matrix m n α, i.e., it is a linear map from α to matrices with entries in α.

Русский

Для фиксированных i, j отображение a ↦ single i j a задаёт линейное отображение α →ₗ[R] Matrix m n α.

LaTeX

$$$ \mathrm{singleLinearMap}_{i j} : α \to\rightarrow_{R} Matrix m n α \\ (\mathrm{singleLinearMap}_{i j})(a) = \mathrm{single}_{i j} a. $$$

Lean4

/-- `Matrix.single` as a bundled linear map. -/
@[simps!]
def singleLinearMap [Semiring R] [AddCommMonoid α] [Module R α] (i : m) (j : n) : α →ₗ[R] Matrix m n α
    where
  __ := singleAddMonoidHom i j
  map_smul' _ _ := smul_single _ _ _ _ |>.symm

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