single — Mathlib

English

For a family f_i of linear maps, the j-th component of f applied to the i-th delta vector equals the j-th coordinate of f_i(x).

Русский

Для семейства линейных отображений f_i, j-ая компонента f( Pi.single_i x ) равна j-ой компоненте f_i(x).

LaTeX

$$$ f_j(\\Pi.single i x) = (\\Pi.single i (f_i x))_j.$$$

Lean4

/-- The `LinearMap` version of `AddMonoidHom.single` and `Pi.single`. -/
def single [DecidableEq ι] (i : ι) : φ i →ₗ[R] (i : ι) → φ i :=
  { AddMonoidHom.single φ i with
    toFun := Pi.single i
    map_smul' := Pi.single_smul i }

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