lmap — Mathlib

English

The linear map lmap f: ⊕ M_i → ⊕ N_i is the direct-sum map induced by the family of linear maps f_i: M_i → N_i; it sends each element to the family (f_i(x_i)).

Русский

Линейное отображение lmap f: ⊕ M_i → ⊕ N_i есть отображение прямой суммы, индуцированное семейством линейных отображений f_i: M_i → N_i; оно отправляет элемент на семью (f_i(x_i)).

LaTeX

$$$\\mathrm{lmap}\\ f : \\bigoplus_i M_i \\to \\bigoplus_i N_i \;\\equiv\\; (x_i) \\mapsto (f_i(x_i))_i.$$$

Lean4

/-- The linear map between direct sums induced by a family of linear maps. -/
def lmap : (⨁ i, M i) →ₗ[R] ⨁ i, N i :=
  DFinsupp.mapRange.linearMap f

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