Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2021-03-10 11:57 ccd35db8

View on Github →

feat(linear_algebra/matrix): to_matrix and to_lin as alg_equiv (#6496) The existing linear_map.to_matrix and matrix.to_lin can be upgraded to an alg_equiv if working on linear endomorphisms or square matrices. The API is copied over in rote fashion.

Estimated changes

Modified src/algebra/algebra/basic.lean

added theorem matrix.algebra_map_eq_smul

Modified src/linear_algebra/matrix.lean

added def linear_map.to_matrix_alg_equiv'

added theorem linear_map.to_matrix_alg_equiv'_apply

added theorem linear_map.to_matrix_alg_equiv'_comp

added theorem linear_map.to_matrix_alg_equiv'_id

added theorem linear_map.to_matrix_alg_equiv'_mul

added theorem linear_map.to_matrix_alg_equiv'_symm

added theorem linear_map.to_matrix_alg_equiv'_to_lin_alg_equiv'

added def linear_map.to_matrix_alg_equiv

added theorem linear_map.to_matrix_alg_equiv_apply'

added theorem linear_map.to_matrix_alg_equiv_apply

added theorem linear_map.to_matrix_alg_equiv_comp

added theorem linear_map.to_matrix_alg_equiv_id

added theorem linear_map.to_matrix_alg_equiv_mul

added theorem linear_map.to_matrix_alg_equiv_range

added theorem linear_map.to_matrix_alg_equiv_symm

added theorem linear_map.to_matrix_alg_equiv_to_lin_alg_equiv

added theorem linear_map.to_matrix_alg_equiv_transpose_apply'

added theorem linear_map.to_matrix_alg_equiv_transpose_apply

added def matrix.to_lin_alg_equiv'

added theorem matrix.to_lin_alg_equiv'_apply

added theorem matrix.to_lin_alg_equiv'_mul

added theorem matrix.to_lin_alg_equiv'_one

added theorem matrix.to_lin_alg_equiv'_symm

added theorem matrix.to_lin_alg_equiv'_to_matrix_alg_equiv'

added def matrix.to_lin_alg_equiv

added theorem matrix.to_lin_alg_equiv_apply

added theorem matrix.to_lin_alg_equiv_mul

added theorem matrix.to_lin_alg_equiv_one

added theorem matrix.to_lin_alg_equiv_self

added theorem matrix.to_lin_alg_equiv_symm

added theorem matrix.to_lin_alg_equiv_to_matrix_alg_equiv