instTwoUniqueProdsOfTwoUniqueSums

English

If M has Add and TwoUniqueSums, then the multiplicative version of M has TwoUniqueProds.

Русский

Если у M есть сложение и свойство TwoUniqueSums, то у M в мультипликативной версии будет TwoUniqueProds.

LaTeX

$$$ \\forall M\\, [\\text{Add }M]\\,[\\text{TwoUniqueSums }M] \\Rightarrow \\mathrm{TwoUniqueProds}(\\mathrm{Multiplicative}\\,M). $$$

Lean4

instance {M} [Add M] [TwoUniqueSums M] : TwoUniqueProds (Multiplicative M) where
  uniqueMul_of_one_lt_card := TwoUniqueSums.uniqueAdd_of_one_lt_card (G := M)

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