instUniqueSumsFinsupp — Mathlib

English

For any index type ι and family G, if AddZeroClass and UniqueSums hold for each G i, then UniqueSums holds for ι →₀ G.

Русский

Для типа индексов ι и семейства G, если для каждого G i выполнены AddZeroClass и UniqueSums, то UniqueSums держится для Finsupp ι G.

LaTeX

$$$ [\\forall i, AddZeroClass (G i)] [\\forall i, UniqueSums (G i)] \\Rightarrow \\mathrm{UniqueSums}(\\iota \\to_0 G), $$$

Lean4

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

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