Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2020-10-26 18:39 61c095f2

View on Github →

chore(algebra/module,linear_algebra): split off a linear_map file (#4476) In order to make algebra/module/basic.lean and linear_algebra/basic.lean a bit more manageable, move the basic facts about linear_maps and linear_equivs into a separate file. linear_algebra/basic.lean still needs to be split a bit more.

Estimated changes

deleted theorem is_linear_map.map_neg
deleted theorem is_linear_map.map_sub
deleted theorem is_linear_map.map_zero
deleted def is_linear_map.mk'
deleted theorem is_linear_map.mk'_apply
deleted structure is_linear_map
deleted theorem linear_map.coe_injective
deleted theorem linear_map.coe_mk
deleted def linear_map.comp
deleted theorem linear_map.comp_apply
deleted theorem linear_map.comp_coe
deleted theorem linear_map.ext
deleted theorem linear_map.ext_iff
deleted theorem linear_map.ext_ring
deleted def linear_map.id
deleted theorem linear_map.id_apply
deleted theorem linear_map.id_coe
deleted theorem linear_map.is_linear
deleted theorem linear_map.map_add
deleted theorem linear_map.map_neg
deleted theorem linear_map.map_smul
deleted theorem linear_map.map_sub
deleted theorem linear_map.map_sum
deleted theorem linear_map.map_zero
deleted theorem linear_map.to_fun_eq_coe
deleted structure linear_map
deleted def module.End
added theorem is_linear_map.map_neg
added theorem is_linear_map.map_sub
added theorem is_linear_map.map_zero
added structure is_linear_map
added theorem linear_equiv.coe_coe
added theorem linear_equiv.comp_coe
added theorem linear_equiv.ext
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_apply
added theorem linear_equiv.symm_symm
added structure linear_equiv
added theorem linear_map.coe_mk
added def linear_map.comp
added theorem linear_map.comp_apply
added theorem linear_map.comp_coe
added theorem linear_map.ext
added theorem linear_map.ext_iff
added theorem linear_map.ext_ring
added def linear_map.id
added theorem linear_map.id_apply
added theorem linear_map.id_coe
added theorem linear_map.is_linear
added theorem linear_map.map_add
added theorem linear_map.map_neg
added theorem linear_map.map_smul
added theorem linear_map.map_sub
added theorem linear_map.map_sum
added theorem linear_map.map_zero
added structure linear_map
added def module.End
deleted theorem linear_equiv.coe_coe
deleted theorem linear_equiv.coe_to_equiv
deleted theorem linear_equiv.comp_coe
deleted theorem linear_equiv.ext
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_apply
deleted def linear_equiv.refl
deleted theorem linear_equiv.refl_apply
deleted theorem linear_equiv.refl_trans
deleted def linear_equiv.symm
deleted theorem linear_equiv.symm_symm
deleted theorem linear_equiv.symm_trans
deleted theorem linear_equiv.to_equiv_inj
deleted theorem linear_equiv.to_fun_apply
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
deleted def linear_map.inverse