equivProdDFinsupp_add — Mathlib

English

EquivProdDFinsupp respects addition: equivProdDFinsupp (f + g) = equivProdDFinsupp f + equivProdDFinsupp g.

Русский

Эквив Prod DFinsupp сохраняет сложение: equivProdDFinsupp (f+g) = equivProdDFinsupp f + equivProdDFinsupp g.

LaTeX

$$$\\mathrm{equivProdDFinsupp}(f+g) = \\mathrm{equivProdDFinsupp}(f) + \\mathrm{equivProdDFinsupp}(g)$$$

Lean4

theorem equivProdDFinsupp_add [∀ i, AddZeroClass (α i)] (f g : Π₀ i, α i) :
    equivProdDFinsupp (f + g) = equivProdDFinsupp f + equivProdDFinsupp g :=
  Prod.ext (add_apply _ _ _) (comapDomain_add _ (Option.some_injective _) _ _)

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