Commit 2021-08-25 06:39 4a0c3d71
View on Github →feat(linear_algebra/finite_dimension): nontriviality lemmas (#8851)
A vector space of finrank greater than zero is nontrivial, likewise a vector space whose finrank is equal to the successor of a natural number.
Also write the non-fact version of finite_dimensional_of_finrank_eq_succ, a lemma which previously existed under a fact hypothesis, and rename the fact version to fact_finite_dimensional_of_finrank_eq_succ.