Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2020-07-10 05:40 bcf733fa

View on Github →

feat(data/matrix): add matrix.map and supporting lemmas (#3352) As requested.

Estimated changes

Modified src/data/matrix/basic.lean

added def add_monoid_hom.map_matrix

added theorem add_monoid_hom.map_matrix_apply

added theorem matrix.diagonal_map

deleted theorem matrix.elementary_eq_basis_mul_basis

added def matrix.map

added theorem matrix.map_add

added theorem matrix.map_apply

added theorem matrix.map_mul

added theorem matrix.map_zero

deleted theorem matrix.matrix_eq_sum_elementary

added theorem matrix.matrix_eq_sum_std_basis

added theorem matrix.one_map

added theorem matrix.std_basis_eq_basis_mul_basis

added theorem matrix.transpose_map

modified theorem matrix.transpose_mul

modified theorem matrix.transpose_neg

modified theorem matrix.transpose_smul

modified theorem matrix.transpose_sub

added def ring_hom.map_matrix

added theorem ring_hom.map_matrix_apply

Modified src/ring_theory/matrix_algebra.lean

deleted theorem matrix_equiv_tensor_apply_elementary

added theorem matrix_equiv_tensor_apply_std_basis

Modified src/ring_theory/polynomial_algebra.lean