UniqueProds

📁 Source: Mathlib/Algebra/FreeMonoid/UniqueProds.lean

Statistics

Metric	Count
Definitions UniqueProds	1
Theorems instTwoUniqueSums, instTwoUniqueProds	2
Total	3

FreeAddMonoid

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
instTwoUniqueSums 📖	mathematical	—	TwoUniqueSums FreeAddMonoid AddSemigroup.toAdd AddMonoid.toAddSemigroup AddRightCancelMonoid.toAddMonoid AddCancelMonoid.toAddRightCancelMonoid instAddCancelMonoid	—	TwoUniqueSums.of_addHom TwoUniqueSums.of_covariant_left AddLeftCancelSemigroup.toIsLeftCancelAdd IsRightCancelAdd.addRightStrictMono_of_addRightMono AddRightCancelSemigroup.toIsRightCancelAdd covariant_swap_add_of_covariant_add IsOrderedAddMonoid.toAddLeftMono Nat.instIsOrderedAddMonoid

FreeMonoid

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
instTwoUniqueProds 📖	mathematical	—	TwoUniqueProds FreeMonoid MulOne.toMul MulOneClass.toMulOne Monoid.toMulOneClass RightCancelMonoid.toMonoid CancelMonoid.toRightCancelMonoid instCancelMonoid	—	TwoUniqueProds.of_mulHom Equiv.injective Multiplicative.instTwoUniqueProdsOfTwoUniqueSums TwoUniqueSums.of_covariant_left AddLeftCancelSemigroup.toIsLeftCancelAdd IsRightCancelAdd.addRightStrictMono_of_addRightMono AddRightCancelSemigroup.toIsRightCancelAdd covariant_swap_add_of_covariant_add IsOrderedAddMonoid.toAddLeftMono Nat.instIsOrderedAddMonoid

(root)

Definitions

Name	Category	Theorems
UniqueProds 📖	CompData	9 math math: Prod.instUniqueProds, UniqueProds.of_injective_mulHom, UniqueProds.of_mulHom, MulEquiv.uniqueProds_iff, UniqueProds.of_mulOpposite, UniqueProds.of_same, UniqueProds.instMulOpposite, TwoUniqueProds.toUniqueProds, Multiplicative.instUniqueProdsOfUniqueSums

---

← Back to Index