Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2021-08-02 10:07 4a9cbdb1

View on Github →

feat(data/matrix/basic): provide equiv versions of matrix.map, linear_map.map_matrix, and ring_hom.map_matrix. (#8468) This moves all of these definitions to be adjacent, adds the standard family of functorial simp lemmas, and relaxes some typeclass requirements. This also renames matrix.one_map to matrix.map_one to match matrix.map_zero.

Estimated changes

Modified src/algebra/algebra/basic.lean

Modified src/data/matrix/basic.lean

added def add_equiv.map_matrix

added theorem add_equiv.map_matrix_refl

added theorem add_equiv.map_matrix_symm

added theorem add_equiv.map_matrix_trans

modified def add_monoid_hom.map_matrix

deleted theorem add_monoid_hom.map_matrix_apply

added theorem add_monoid_hom.map_matrix_comp

added theorem add_monoid_hom.map_matrix_id

added def equiv.map_matrix

added theorem equiv.map_matrix_refl

added theorem equiv.map_matrix_symm

added theorem equiv.map_matrix_trans

added def linear_equiv.map_matrix

added theorem linear_equiv.map_matrix_refl

added theorem linear_equiv.map_matrix_symm

added theorem linear_equiv.map_matrix_trans

modified def linear_map.map_matrix

added theorem linear_map.map_matrix_comp

added theorem linear_map.map_matrix_id

modified theorem matrix.map_add

added theorem matrix.map_id

added theorem matrix.map_one

modified theorem matrix.map_smul

modified theorem matrix.map_sub

modified theorem matrix.map_zero

deleted theorem matrix.one_map

added def ring_equiv.map_matrix

added theorem ring_equiv.map_matrix_refl

added theorem ring_equiv.map_matrix_symm

added theorem ring_equiv.map_matrix_trans

modified def ring_hom.map_matrix

added theorem ring_hom.map_matrix_comp

added theorem ring_hom.map_matrix_id