Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2021-09-22 01:01 5625ec02

View on Github →

refactor(algebra/module/linear_map): Put linear equivalences in their own file (#9301) This is consistent with how we have ring homs and ring equivs in separate files. By having each of these files smaller than the original, we can split linear_algebra/basic more effectively between them.

Estimated changes

deleted theorem linear_equiv.coe_coe
deleted theorem linear_equiv.coe_mk
deleted theorem linear_equiv.coe_symm_mk
deleted theorem linear_equiv.coe_to_equiv
deleted theorem linear_equiv.comp_coe
deleted theorem linear_equiv.ext
deleted theorem linear_equiv.ext_iff
deleted theorem linear_equiv.map_add
deleted theorem linear_equiv.map_smul
deleted theorem linear_equiv.map_sum
deleted theorem linear_equiv.map_zero
deleted theorem linear_equiv.mk_coe'
deleted theorem linear_equiv.mk_coe
deleted def linear_equiv.refl
deleted theorem linear_equiv.refl_apply
deleted theorem linear_equiv.refl_symm
deleted theorem linear_equiv.refl_trans
deleted def linear_equiv.symm
deleted theorem linear_equiv.symm_mk
deleted theorem linear_equiv.symm_symm
deleted theorem linear_equiv.symm_trans
deleted theorem linear_equiv.to_equiv_inj
deleted def linear_equiv.trans
deleted theorem linear_equiv.trans_apply
deleted theorem linear_equiv.trans_refl
deleted theorem linear_equiv.trans_symm
deleted structure linear_equiv
added theorem linear_equiv.coe_coe
added theorem linear_equiv.coe_mk
added theorem linear_equiv.comp_coe
added theorem linear_equiv.ext
added theorem linear_equiv.ext_iff
added theorem linear_equiv.map_add
added theorem linear_equiv.map_smul
added theorem linear_equiv.map_sum
added theorem linear_equiv.map_zero
added theorem linear_equiv.mk_coe'
added theorem linear_equiv.mk_coe
added theorem linear_equiv.refl_symm
added theorem linear_equiv.symm_mk
added theorem linear_equiv.symm_symm
added structure linear_equiv