instUniqueProdsOfUniqueSums — Mathlib

English

Let M be a type equipped with an additive structure and the property UniqueSums. Then turning M into a multiplicative structure yields the property UniqueProds.

Русский

Пусть M — множество с операцией сложения и свойством UniqueSums. Тогда, рассматривая M как множество с умножением (Multiplicative M), выполняется свойство UniqueProds.

LaTeX

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

Lean4

instance {M} [Add M] [UniqueSums M] : UniqueProds (Multiplicative M) where
  uniqueMul_of_nonempty := UniqueSums.uniqueAdd_of_nonempty (G := M)

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