finsupp_dom — Mathlib

English

A specialization of the previous identity where the maps are linear, giving the same pulling-out property for sums.

Русский

Специализация предыдущей идеи на линейные отображения даёт то же свойство извлечения множителя из суммы.

LaTeX

$$$$ ((c \cdot v).sum h) = c \cdot (v.sum h). $$$$

Lean4

instance _root_.LinearMap.CompatibleSMul.finsupp_dom [SMulZeroClass R M] [DistribSMul R N]
    [LinearMap.CompatibleSMul M N R S] : LinearMap.CompatibleSMul (ι →₀ M) N R S where
  map_smul f r
    m := by
    conv_rhs => rw [← sum_single m, map_finsuppSum, smul_sum]
    erw [← sum_single (r • m), sum_mapRange_index single_zero, map_finsuppSum]
    congr; ext i m; exact (f.comp <| lsingle i).map_smul_of_tower r m

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