VectorSpace

📁 Source: Mathlib/Algebra/Group/UniqueProds/VectorSpace.lean

Statistics

Metric	Count
Definitions	0
Theorems instTwoUniqueSumsOfModuleRat	1
Total	1

(root)

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
instTwoUniqueSumsOfModuleRat 📖	mathematical	—	TwoUniqueSums AddCommMagma.toAdd AddCommSemigroup.toAddCommMagma AddCommMonoid.toAddCommSemigroup AddCommGroup.toAddCommMonoid	—	TwoUniqueSums.of_injective_addHom RingHomInvPair.ids LinearEquiv.injective instTwoUniqueSumsFinsupp TwoUniqueSums.of_covariant_left AddLeftCancelSemigroup.toIsLeftCancelAdd IsRightCancelAdd.addRightStrictMono_of_addRightMono AddRightCancelSemigroup.toIsRightCancelAdd covariant_swap_add_of_covariant_add Rat.instAddLeftMono

---

← Back to Index