Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2022-04-25 05:10 070c21b6

View on Github →

chore(data/matrix): generalisation linter (#13655)

Estimated changes

Modified src/data/matrix/basic.lean

modified theorem matrix.col_mul_vec

modified theorem matrix.col_vec_mul

modified theorem matrix.conj_transpose_mul

modified theorem matrix.conj_transpose_neg

modified theorem matrix.conj_transpose_smul

modified theorem matrix.conj_transpose_zero

modified theorem matrix.diagonal_conj_transpose

modified theorem matrix.dot_product_comm

modified theorem matrix.minor_mul

modified theorem matrix.minor_mul_equiv

modified theorem matrix.minor_mul_transpose_minor

modified theorem matrix.minor_smul

modified theorem matrix.minor_zero

modified theorem matrix.mul_minor_one

modified theorem matrix.mul_vec_smul

modified theorem matrix.one_minor_mul

modified theorem matrix.row_mul_vec

modified theorem matrix.row_vec_mul

modified theorem matrix.star_mul

modified theorem matrix.transpose_mul

modified def matrix.transpose_ring_equiv

modified theorem matrix.vec_mul_smul

modified theorem matrix.vec_mul_vec_eq

modified theorem ring_hom.map_dot_product

modified theorem ring_hom.map_mul_vec

modified theorem ring_hom.map_vec_mul