instTwoUniqueSumsFinsupp — Mathlib

English

If G is an additive structure with AddZeroClass and TwoUniqueSums, then the space Finsupp(I, G) of finitely supported functions from I to G also has TwoUniqueSums.

Русский

Если G — добавочная структура с AddZeroClass и TwoUniqueSums, то пространство Finsupp(I, G) конечной поддержки также обладает TwoUniqueSums.

LaTeX

$$$\forall I\; \forall G\;\big(\text{AddZeroClass}(G) \wedge \text{TwoUniqueSums}(G)\big) \Rightarrow \text{TwoUniqueSums}(\mathrm{Finsupp}_{I} G)$$$

Lean4

instance {ι G} [AddZeroClass G] [TwoUniqueSums G] : TwoUniqueSums (ι →₀ G) :=
  TwoUniqueSums.of_injective_addHom Finsupp.coeFnAddHom.toAddHom DFunLike.coe_injective inferInstance

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