instTwoUniqueSumsFreeAbelianGroup

English

There is a TwoUniqueSums structure on FreeAbelianGroup σ, inherited from the Finsupp equivalence.

Русский

Для свободной абелевой группы над σ существует структура TwoUniqueSums, наследованная от эквивалентности с Finsupp.

LaTeX

$$TwoUniqueSums (FreeAbelianGroup σ)$$

Lean4

instance {σ : Type*} : TwoUniqueSums (FreeAbelianGroup σ) :=
  (FreeAbelianGroup.equivFinsupp σ).twoUniqueSums_iff.mpr inferInstance

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