Commit 2021-09-06 21:09 309674d9
View on Github →feat(linear_algebra/basis): a nontrivial module has nonempty bases (#9040) A tiny little lemma that guarantees the dimension of a nontrivial module is nonzero. Noticeably simplifies the proof that the dimension of a power basis is positive in this case.