VectorSpace

Statistics

Metric	Count
Definitions	0
Theorems `instTwoUniqueSumsOfModuleRat`	1
Total	1

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` `instIsLeftCancelAddOfAddLeftReflectLE` `AddGroup.covconv` `Rat.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`

---