finsupp_cod — Mathlib

English

The canonical representation of the linear equivalence lsum corresponds to the sum decomposition of Finsupp maps.

Русский

Каноническое представление линейного эквивалента lsum соответствует разложению по сумме отображений Finsupp.

LaTeX

$$$$ \operatorname{coe}_{\text{lsum}}(f) = (d \mapsto \sum_i f_i(d)) $$$$

Lean4

instance _root_.LinearMap.CompatibleSMul.finsupp_cod [SMul R M] [SMulZeroClass R N] [LinearMap.CompatibleSMul M N R S] :
    LinearMap.CompatibleSMul M (ι →₀ N) R S where
  map_smul f r m := by ext i; apply ((lapply i).comp f).map_smul_of_tower

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