Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2020-06-22 10:46 105fa176

View on Github →

feat(linear_algebra/matrix): trace of an endomorphism independent of basis (#3125)

Estimated changes

Modified src/data/equiv/basic.lean

added theorem equiv.of_injective_apply

Modified src/linear_algebra/basic.lean

added theorem linear_equiv.arrow_congr_trans

added theorem linear_equiv.symm_trans_apply

added def linear_map.fun_congr_left

added theorem linear_map.fun_congr_left_apply

added theorem linear_map.fun_congr_left_comp

added theorem linear_map.fun_congr_left_id

added theorem linear_map.fun_congr_left_symm

added def linear_map.fun_left

added theorem linear_map.fun_left_apply

added theorem linear_map.fun_left_comp

added theorem linear_map.fun_left_id

Modified src/linear_algebra/basis.lean

added theorem is_basis.range

Modified src/linear_algebra/matrix.lean

added theorem linear_equiv_matrix'_apply

added theorem linear_equiv_matrix_range

added theorem linear_map.to_matrix_of_equiv

added def linear_map.trace

added def linear_map.trace_aux

added theorem linear_map.trace_aux_def

added theorem linear_map.trace_aux_eq'

added theorem linear_map.trace_aux_eq

added theorem linear_map.trace_aux_range

added theorem linear_map.trace_eq_matrix_trace

added theorem linear_map.trace_mul_comm

added theorem matrix.linear_equiv_matrix_comp

added theorem matrix.linear_equiv_matrix_mul

added theorem matrix.to_lin_of_equiv