mathlib3

500ccb10 - chore(linear_algebra/dimension): remove a nontriviality assumption (#18715)

chore(linear_algebra/dimension): remove a nontriviality assumption (#18715) `dim_pos` does not need `nontrivial R`. Also adds a new lemma that demonstrates why the assumption is still needed on some later results.