equivProdDFinsupp_smul — Mathlib

English

For all r in γ and f in DFinsupp, equivProdDFinsupp(r • f) equals r • equivProdDFinsupp f; i.e., the equivProdDFinsupp is γ-linear with respect to smul.

Русский

Для всех элементов r из γ и f из DFinsupp выполняется равенство equivProdDFinsupp(r • f) = r • equivProdDFinsupp f; то есть отображение equivProdDFinsupp линейно по γ.

LaTeX

$$$$ \\operatorname{equivProdDFinsupp}\\left(r\\cdot f\\right) = r\\cdot \\operatorname{equivProdDFinsupp}(f). $$$$

Lean4

theorem equivProdDFinsupp_smul [∀ i, Zero (α i)] [∀ i, SMulZeroClass γ (α i)] (r : γ) (f : Π₀ i, α i) :
    equivProdDFinsupp (r • f) = r • equivProdDFinsupp f :=
  Prod.ext (smul_apply _ _ _) (comapDomain_smul _ (Option.some_injective _) _ _)

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