English
The LinearMap single is the embedding that places an element x in the i-th coordinate and zeros elsewhere; it coincides with the standard Pi.single map.
Русский
Линейное отображение single вставляет элемент x в i-ю координату и зануляет остальные; оно совпадает с обычной Pi.single картой.
LaTeX
$$$\\text{single}_i(x)= (\\delta_{j,i} x)_{j\\in \\iota} = \\Pi\\text{single}_i(x).$$$
Lean4
/-- Linear map between the function spaces `I → M₂` and `I → M₃`, induced by a linear map `f`
between `M₂` and `M₃`. -/
@[simps]
protected def compLeft (f : M₂ →ₗ[R] M₃) (I : Type*) : (I → M₂) →ₗ[R] I → M₃ :=
{ f.toAddMonoidHom.compLeft I with
toFun := fun h => f ∘ h
map_smul' := fun c h => by
ext x
exact f.map_smul' c (h x) }
