Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2021-05-10 07:36 b5776971

View on Github →

feat(data/matrix/basic): add missing smul instances, generalize lemmas to work on scalar towers (#7544) This also fixes the add_monoid_hom.map_zero etc lemmas to not require overly strong typeclasses on α This removes the matrix.smul_apply lemma since pi.smul_apply and smul_eq_mul together replace it.

Estimated changes

modified theorem matrix.add_equiv_map_zero
modified theorem matrix.diagonal_map
modified theorem matrix.dot_product_smul
modified theorem matrix.linear_map_map_zero
modified def matrix.map
modified theorem matrix.map_add
modified theorem matrix.map_apply
modified theorem matrix.map_mul
modified theorem matrix.map_sub
modified theorem matrix.map_zero
modified theorem matrix.mul_smul
modified theorem matrix.one_map
modified theorem matrix.ring_equiv_map_one
modified theorem matrix.ring_equiv_map_zero
modified theorem matrix.ring_hom_map_one
modified theorem matrix.ring_hom_map_zero
deleted theorem matrix.smul_apply
modified theorem matrix.smul_dot_product
modified theorem matrix.smul_mul
modified theorem matrix.star_apply
modified theorem matrix.star_mul
modified theorem matrix.transpose_map
modified theorem matrix.zero_hom_map_zero
modified def ring_hom.map_matrix
deleted theorem ring_hom.map_matrix_apply