Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2022-04-19 20:26 094b1f51

View on Github →

chore(*/matrix): order m and n alphabetically (#13510) In a few places this also reorders (n) [fintype n] (m) [fintype m] to (m n) [fintype m] [fintype n] which seems to be where we prefer to put typeclasses.

Estimated changes

modified theorem matrix.nnnorm_le_iff
modified theorem matrix.nnnorm_lt_iff
modified theorem matrix.norm_le_iff
modified theorem matrix.norm_lt_iff
modified theorem matrix.map_update_column
modified theorem matrix.map_update_row
modified def matrix.update_column
modified theorem matrix.update_column_apply
modified theorem matrix.update_column_ne
modified theorem matrix.update_column_self
modified def matrix.update_row
modified theorem matrix.update_row_apply
modified theorem matrix.update_row_ne
modified theorem matrix.update_row_self
modified theorem matrix.update_row_transpose
modified theorem matrix.vec_mul_smul
modified theorem module.free.finrank_matrix
modified theorem module.free.rank_matrix''
modified theorem module.free.rank_matrix'
modified theorem module.free.rank_matrix
modified theorem continuous.matrix_map
modified theorem continuous.matrix_transpose