Commit 2024-07-01 08:42 f9f5cd90

View on Github →

chore(Algebra/Module/LinearMap): split into Basic and Defs (#14226) There is nothing fancy about the split; just everything that is okay with the minimal imports for the important definitions has stayed in Defs. Very happy if anyone wants to follow-up with fine-grained rearrangements.

Estimated changes

deleted theorem IsLinearMap.map_neg
deleted theorem IsLinearMap.map_sub
deleted theorem IsLinearMap.map_zero
deleted def IsLinearMap.mk'
deleted theorem IsLinearMap.mk'_apply
deleted structure IsLinearMap
deleted theorem LinearMap.add_apply
deleted theorem LinearMap.add_comp
deleted theorem LinearMap.cancel_left
deleted theorem LinearMap.cancel_right
deleted theorem LinearMap.coe_addHom_mk
deleted theorem LinearMap.coe_coe
deleted theorem LinearMap.coe_comp
deleted theorem LinearMap.coe_copy
deleted theorem LinearMap.coe_injective
deleted theorem LinearMap.coe_mk
deleted theorem LinearMap.coe_smul
deleted theorem LinearMap.coe_toAddHom
deleted def LinearMap.comp
deleted theorem LinearMap.comp_add
deleted theorem LinearMap.comp_apply
deleted theorem LinearMap.comp_assoc
deleted theorem LinearMap.comp_id
deleted theorem LinearMap.comp_neg
deleted theorem LinearMap.comp_smul
deleted theorem LinearMap.comp_sub
deleted theorem LinearMap.comp_zero
deleted theorem LinearMap.copy_eq
deleted theorem LinearMap.default_def
deleted theorem LinearMap.ext
deleted theorem LinearMap.ext_iff
deleted theorem LinearMap.ext_ring
deleted theorem LinearMap.ext_ring_iff
deleted theorem LinearMap.ext_ring_op
deleted def LinearMap.id'
deleted theorem LinearMap.id'_coe
deleted def LinearMap.id
deleted theorem LinearMap.id_apply
deleted theorem LinearMap.id_coe
deleted theorem LinearMap.id_comp
deleted def LinearMap.inverse
deleted theorem LinearMap.isLinear
deleted theorem LinearMap.map_eq_zero_iff
deleted theorem LinearMap.mk_coe
deleted theorem LinearMap.neg_apply
deleted theorem LinearMap.neg_comp
deleted theorem LinearMap.smul_apply
deleted theorem LinearMap.smul_comp
deleted theorem LinearMap.sub_apply
deleted theorem LinearMap.sub_comp
deleted theorem LinearMap.toFun_eq_coe
deleted theorem LinearMap.zero_apply
deleted theorem LinearMap.zero_comp
deleted structure LinearMap
added theorem IsLinearMap.map_neg
added theorem IsLinearMap.map_sub
added theorem IsLinearMap.map_zero
added def IsLinearMap.mk'
added theorem IsLinearMap.mk'_apply
added structure IsLinearMap
added theorem LinearMap.add_apply
added theorem LinearMap.add_comp
added theorem LinearMap.cancel_left
added theorem LinearMap.cancel_right
added theorem LinearMap.coe_coe
added theorem LinearMap.coe_comp
added theorem LinearMap.coe_copy
added theorem LinearMap.coe_mk
added theorem LinearMap.coe_smul
added theorem LinearMap.coe_toAddHom
added def LinearMap.comp
added theorem LinearMap.comp_add
added theorem LinearMap.comp_apply
added theorem LinearMap.comp_assoc
added theorem LinearMap.comp_id
added theorem LinearMap.comp_neg
added theorem LinearMap.comp_smul
added theorem LinearMap.comp_sub
added theorem LinearMap.comp_zero
added theorem LinearMap.copy_eq
added theorem LinearMap.default_def
added theorem LinearMap.ext
added theorem LinearMap.ext_iff
added theorem LinearMap.ext_ring
added theorem LinearMap.ext_ring_iff
added theorem LinearMap.ext_ring_op
added def LinearMap.id'
added theorem LinearMap.id'_coe
added def LinearMap.id
added theorem LinearMap.id_apply
added theorem LinearMap.id_coe
added theorem LinearMap.id_comp
added theorem LinearMap.isLinear
added theorem LinearMap.mk_coe
added theorem LinearMap.neg_apply
added theorem LinearMap.neg_comp
added theorem LinearMap.smul_apply
added theorem LinearMap.smul_comp
added theorem LinearMap.sub_apply
added theorem LinearMap.sub_comp
added theorem LinearMap.toFun_eq_coe
added theorem LinearMap.zero_apply
added theorem LinearMap.zero_comp
added structure LinearMap