toUniqueProds — Mathlib

English

If a type G has TwoUniqueProds, then it has UniqueProds; the two-unique-product condition implies the unique-product condition.

Русский

Если у типа G есть TwoUniqueProds, то он имеет UniqueProds; условие двух уникальных произведений влечет условие уникального произведения.

LaTeX

$$$\\text{TwoUniqueProds}\\,G \\Rightarrow \\text{UniqueProds}\\,G$$$

Lean4

@[to_additive]
instance toUniqueProds (G) [Mul G] [TwoUniqueProds G] : UniqueProds G where
  uniqueMul_of_nonempty := uniqueMul_of_twoUniqueMul uniqueMul_of_one_lt_card

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