instUniqueSumsOfUniqueProds — Mathlib

English

If a multiplicative structure on M has UniqueProds, then the corresponding additive structure Additive M has UniqueSums.

Русский

Если в M с умножением есть свойство UniqueProds, тогда в Additive M получаем UniqueSums.

LaTeX

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

Lean4

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

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