UniqueSums

📁 Source: Mathlib/Algebra/FreeAbelianGroup/UniqueSums.lean

Statistics

Metric	Count
Definitions UniqueSums	1
Theorems instTwoUniqueSumsFreeAbelianGroup	1
Total	2

(root)

Definitions

Name	Category	Theorems
UniqueSums 📖	CompData	10 math math: TwoUniqueSums.toUniqueSums, AddEquiv.uniqueSums_iff, UniqueSums.of_injective_addHom, Prod.instUniqueSums, Additive.instUniqueSumsOfUniqueProds, UniqueSums.of_same, UniqueSums.of_addHom, UniqueSums.instAddOpposite, instUniqueSumsFinsupp, UniqueSums.of_addOpposite

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
instTwoUniqueSumsFreeAbelianGroup 📖	mathematical	—	TwoUniqueSums FreeAbelianGroup AddCommMagma.toAdd AddCommSemigroup.toAddCommMagma AddCommMonoid.toAddCommSemigroup AddCommGroup.toAddCommMonoid FreeAbelianGroup.addCommGroup	—	AddEquiv.twoUniqueSums_iff instTwoUniqueSumsFinsupp TwoUniqueSums.of_covariant_left AddLeftCancelSemigroup.toIsLeftCancelAdd IsRightCancelAdd.addRightStrictMono_of_addRightMono AddRightCancelSemigroup.toIsRightCancelAdd covariant_swap_add_of_covariant_add Int.instAddLeftMono

---

← Back to Index