mathlib

309674d9 - feat(linear_algebra/basis): a nontrivial module has nonempty bases (#9040)

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.