Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2020-08-20 23:05 36386fc7

View on Github →

feat(linear_algebra): some easy linear map/equiv lemmas (#3890) From the sphere eversion project.

Estimated changes

Modified src/linear_algebra/basic.lean

added theorem linear_equiv.comp_coe

added theorem linear_equiv.eq_of_linear_map_eq

added theorem linear_equiv.refl_to_linear_map

added theorem linear_equiv.symm_trans

added theorem linear_equiv.trans_symm

Modified src/linear_algebra/basis.lean

added theorem equiv_of_is_basis_comp

added theorem equiv_of_is_basis_refl

added theorem equiv_of_is_basis_symm_trans

added theorem equiv_of_is_basis_trans_symm