Subsingleton

Statistics

Metric	Count
Definitions	0
Theorems `rank_bot`, `rank_punit`, `rank_subsingleton'`	3
Total	3

Name	Kind	Assumes	Proves	Validates	Depends On
`rank_bot` 📖	mathematical	—	`Module.rank` `Submodule` `SetLike.instMembership` `Submodule.setLike` `Bot.bot` `Submodule.instBot` `Submodule.addCommMonoid` `Submodule.module` `Cardinal` `Cardinal.instZero`	—	`rank_subsingleton'` `Unique.instSubsingleton`
`rank_punit` 📖	mathematical	—	`Module.rank` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `CommRing.toNonUnitalCommRing` `PUnit.commRing` `PUnit.module` `Cardinal` `Cardinal.instZero`	—	`rank_subsingleton'`
`rank_subsingleton'` 📖	mathematical	—	`Module.rank` `Cardinal` `Cardinal.instZero`	—	`Module.rank_def` `bot_eq_zero` `Cardinal.canonicallyOrderedAdd` `eq_bot_iff` `ciSup_le` `nonempty_linearIndependent_set` `Cardinal.mk_eq_zero` `linearIndependent_subsingleton_iff` `bot_eq_zero'`

---