Rank

Statistics

Metric	Count
Definitions	0
Theorems `isSimpleModule_iff_finrank_eq_one`	1
Total	1

Name	Kind	Assumes	Proves	Validates	Depends On
`isSimpleModule_iff_finrank_eq_one` 📖	mathematical	—	`IsSimpleModule` `DivisionRing.toRing` `Module.finrank` `DivisionSemiring.toSemiring` `DivisionRing.toDivisionSemiring` `AddCommGroup.toAddCommMonoid`	—	`IsSimpleModule.nontrivial` `exists_ne` `finrank_eq_one_iff_of_nonzero'` `IsSimpleModule.toSpanSingleton_surjective` `isSimpleModule_iff` `is_simple_module_of_finrank_eq_one` `IsScalarTower.left`

---