Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2021-12-18 16:15 59152548

View on Github →

feat(data/matrix/rank): rank of a matrix (#10826)

Estimated changes

Modified docs/undergrad.yaml

Created src/data/matrix/rank.lean

added theorem matrix.rank_eq_finrank_range_to_lin

added theorem matrix.rank_le_card_height

added theorem matrix.rank_le_card_width

added theorem matrix.rank_le_height

added theorem matrix.rank_le_width

added theorem matrix.rank_mul_le

added theorem matrix.rank_of_is_unit

added theorem matrix.rank_one

added theorem matrix.rank_unit

added theorem matrix.rank_zero

Modified src/linear_algebra/matrix/to_lin.lean