UniqueSums

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

Statistics

Metric	Count
Definitions	0
Theorems to_twoUniqueSums, to_twoUniqueProds	2
Total	2

AffineAddMonoid

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
to_twoUniqueSums 📖	mathematical	—	TwoUniqueSums AddCommMagma.toAdd AddCommSemigroup.toAddCommMagma AddCommMonoid.toAddCommSemigroup AddCancelCommMonoid.toAddCommMonoid	—	TwoUniqueSums.of_injective_addHom embedding_injective instTwoUniqueSumsFreeAbelianGroup

AffineMonoid

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
to_twoUniqueProds 📖	mathematical	—	TwoUniqueProds MulOne.toMul MulOneClass.toMulOne Monoid.toMulOneClass CommMonoid.toMonoid CancelCommMonoid.toCommMonoid	—	Multiplicative.instTwoUniqueProdsOfTwoUniqueSums AffineAddMonoid.to_twoUniqueSums AddMonoid.fg_of_monoid_fg instIsAddTorsionFreeAdditiveOfIsMulTorsionFree

---

← Back to Index