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	12 math math: TwoUniqueSums.toUniqueSums, AddEquiv.uniqueSums_iff, UniqueSums.of_injective_addHom, Prod.instUniqueSums, Additive.instUniqueSumsOfUniqueProds, UniqueSums.of_same, UniqueSums.of_addHom, instUniqueSumsDFinsupp, UniqueSums.instForall, 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 instAddCommGroupFreeAbelianGroup	—	AddEquiv.twoUniqueSums_iff instTwoUniqueSumsFinsupp TwoUniqueSums.of_covariant_left instIsLeftCancelAddOfAddLeftReflectLE AddGroup.covconv Int.instAddLeftMono IsRightCancelAdd.addRightStrictMono_of_addRightMono instIsRightCancelAddOfAddRightReflectLE contravariant_swap_add_of_contravariant_add IsLeftCancelAdd.addLeftReflectLE_of_addLeftReflectLT contravariant_lt_of_covariant_le covariant_swap_add_of_covariant_add

---

← Back to Index