Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2023-04-08 13:17 8535b76e

View on Github →

feat(linear_algebra/matrix/rank): generalize to rings (#18748) This addresses a TODO comment. To achieve this we generalize submodule.finrank_le, submodule.finrank_quotient_le, and finrank_le_finrank_of_injective from vector spaces to free modules, and add a new lemma linear_map.finrank_range_le.

Estimated changes

modified theorem matrix.rank_le_card_height
modified theorem matrix.rank_le_card_width
modified theorem matrix.rank_le_height
modified theorem matrix.rank_le_width
modified theorem matrix.rank_mul_le
modified theorem matrix.rank_of_is_unit
modified theorem matrix.rank_one
modified theorem matrix.rank_unit
modified theorem matrix.rank_zero
deleted theorem submodule.finrank_le
added theorem submodule.finrank_le