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 instIsLeftCancelAddOfAddLeftReflectLE IsOrderedCancelAddMonoid.toAddLeftReflectLE Nat.instIsOrderedCancelAddMonoid IsRightCancelAdd.addRightStrictMono_of_addRightMono instIsRightCancelAddOfAddRightReflectLE contravariant_swap_add_of_contravariant_add IsLeftCancelAdd.addLeftReflectLE_of_addLeftReflectLT contravariant_lt_of_covariant_le IsOrderedAddMonoid.toAddLeftMono Nat.instIsOrderedAddMonoid covariant_swap_add_of_covariant_add

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 instIsLeftCancelAddOfAddLeftReflectLE IsOrderedCancelAddMonoid.toAddLeftReflectLE Nat.instIsOrderedCancelAddMonoid IsRightCancelAdd.addRightStrictMono_of_addRightMono instIsRightCancelAddOfAddRightReflectLE contravariant_swap_add_of_contravariant_add IsLeftCancelAdd.addLeftReflectLE_of_addLeftReflectLT contravariant_lt_of_covariant_le IsOrderedAddMonoid.toAddLeftMono Nat.instIsOrderedAddMonoid covariant_swap_add_of_covariant_add

(root)

Definitions

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

---

← Back to Index