Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2020-08-22 13:26 aca785a7

View on Github →

feat(linear_algebra): linear_equiv_matrix lemmas (#3898) From the sphere eversion project, with help by Anne for the crucial linear_equiv_matrix_apply.

Estimated changes

added theorem linear_map.comp_coe
modified theorem linear_map.id_apply
added theorem linear_map.id_coe
modified def linear_equiv_matrix
added theorem linear_equiv_matrix_id
modified theorem linear_equiv_matrix_range