Commit 2023-05-03 01:24 0a184b93

View on Github →

feat: port Data.Matrix.Rank (#3762)

Estimated changes

Modified Mathlib.lean

Created Mathlib/Data/Matrix/Rank.lean

added theorem Matrix.ker_mulVecLin_conjTranspose_mul_self

added theorem Matrix.ker_mulVecLin_transpose_mul_self

added theorem Matrix.rank_conjTranspose

added theorem Matrix.rank_conjTranspose_mul_self

added theorem Matrix.rank_eq_finrank_range_toLin

added theorem Matrix.rank_eq_finrank_span_cols

added theorem Matrix.rank_eq_finrank_span_row

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_mul_le_left

added theorem Matrix.rank_mul_le_right

added theorem Matrix.rank_of_isUnit

added theorem Matrix.rank_one

added theorem Matrix.rank_reindex

added theorem Matrix.rank_self_mul_conjTranspose

added theorem Matrix.rank_self_mul_transpose

added theorem Matrix.rank_submatrix

added theorem Matrix.rank_submatrix_le

added theorem Matrix.rank_transpose

added theorem Matrix.rank_transpose_mul_self

added theorem Matrix.rank_unit

added theorem Matrix.rank_zero