Mathlib v3 is deprecated. Go to Mathlib v4

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.

Estimated changes

modified theorem dim_pos
modified theorem dim_pos_iff_exists_ne_zero
modified theorem dim_pos_iff_nontrivial
modified theorem dim_zero_iff
modified theorem dim_zero_iff_forall_zero