Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2020-06-13 07:27 1645542c

View on Github →

feat(linear_algebra): elements of a dim zero space (#3054)

Estimated changes

Modified src/linear_algebra/dimension.lean

added theorem dim_pos_iff_exists_ne_zero

added theorem dim_zero_iff_forall_zero

Modified src/linear_algebra/finite_dimensional.lean

added theorem bot_eq_top_of_dim_eq_zero

added theorem findim_bot

added theorem findim_eq_zero_of_dim_eq_zero

added theorem finite_dimensional_bot

added theorem finite_dimensional_of_dim_eq_zero

Modified src/set_theory/cardinal.lean

added theorem cardinal.mk_emptyc_iff