Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2019-01-22 16:49 edfa2061

View on Github →

feat(linear_algebra/dimension): more dimension theorems; rank of a linear map

Estimated changes

added theorem is_basis_empty
added theorem is_basis_empty_bot
added theorem is_basis_injective
added theorem is_basis_span
added theorem dim_add_le_dim_add_dim
added theorem dim_bot
added theorem dim_eq_injective
added theorem dim_eq_surjective
added theorem dim_le_injective
added theorem dim_le_of_submodule
added theorem dim_le_surjective
added theorem dim_map_le
added theorem dim_range_le
added theorem dim_span
added theorem dim_submodule_le
added def rank
added theorem rank_add_le
added theorem rank_comp_le1
added theorem rank_comp_le2
added theorem rank_le_domain
added theorem rank_le_range