← Mathematical handbook

Free monoids have unique products

instance FreeMonoid.instTwoUniqueProds {κ : Type u_1} : TwoUniqueProds (FreeMonoid κ)

Any FreeMonoid has the TwoUniqueProds property.

instance FreeAddMonoid.instTwoUniqueSums {κ : Type u_1} : TwoUniqueSums (FreeAddMonoid κ)

Any FreeAddMonoid has the TwoUniqueSums property.