Commit 2021-10-15 15:08 d6fd5f5f
View on Github →feat(linear_algebra/dimension): generalize dim_zero_iff_forall_zero (#9713)
We generalize dim_zero_iff_forall_zero
to [nontrivial R] [no_zero_smul_divisors R M]
.
If you see a more general class to consider let me know.