Theorems · Theorem · group theory

UniqueProds.toTwoUniqueProds_of_group

∀ {G : Type u_1} [inst : Group G] [UniqueProds G], TwoUniqueProds G

If a group has UniqueProds, then it actually has TwoUniqueProds. For an example of a semigroup G embeddable into a group that has UniqueProds but not TwoUniqueProds, see Example 10.13 in [J. Okniński, Semigroup Algebras][Okninski1991].

Defined in

Mathlib.Algebra.Group.UniqueProds.Basic

Cited by

0 results in Mathlib

Foundations

Depth 81 from the axioms · uses propext, Classical.choice, Quot.sound

Assumes

GroupUniqueProds