instTwoUniqueSumsOfTwoUniqueProds

English

If a multiplicative structure on M has TwoUniqueProds, then the additive structure Additive M has TwoUniqueSums.

Русский

Если в M с умножением есть TwoUniqueProds, тогда в Additive M имеет место TwoUniqueSums.

LaTeX

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

Lean4

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

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