Commit 2023-04-02 16:48 500ccb10
View on Github →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.