Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2021-09-30 16:11 118e809b

View on Github →

refactor(algebra/module/linear_map): Move elementwise structure from linear_algebra/basic (#9331) This helps reduce the size of linear_algebra/basic, and by virtue of being a smaller file makes it easier to spot typeclasses which can be relaxed. As an example, linear_map.endomorphism_ring now requires only semiring R not ring R. Having instances available as early as possible is generally good, as otherwise it is hard to even state things elsewhere.

Estimated changes

added theorem linear_map.add_apply
added theorem linear_map.add_comp
added theorem linear_map.coe_mul
added theorem linear_map.coe_one
added theorem linear_map.comp_add
added theorem linear_map.comp_neg
added theorem linear_map.comp_smul
added theorem linear_map.comp_sub
added theorem linear_map.comp_zero
added theorem linear_map.default_def
added theorem linear_map.mul_apply
added theorem linear_map.mul_eq_comp
added theorem linear_map.neg_apply
added theorem linear_map.neg_comp
added theorem linear_map.one_apply
added theorem linear_map.one_eq_id
added theorem linear_map.smul_apply
added theorem linear_map.smul_comp
added theorem linear_map.sub_apply
added theorem linear_map.sub_comp
added theorem linear_map.zero_apply
added theorem linear_map.zero_comp
deleted theorem linear_map.add_apply
deleted theorem linear_map.add_comp
deleted theorem linear_map.coe_mul
deleted theorem linear_map.coe_one
deleted theorem linear_map.comp_add
deleted theorem linear_map.comp_neg
deleted theorem linear_map.comp_smul
deleted theorem linear_map.comp_sub
deleted theorem linear_map.comp_zero
deleted theorem linear_map.default_def
deleted theorem linear_map.mul_apply
deleted theorem linear_map.mul_eq_comp
deleted theorem linear_map.neg_apply
deleted theorem linear_map.neg_comp
deleted theorem linear_map.one_apply
deleted theorem linear_map.one_eq_id
deleted theorem linear_map.smul_apply
deleted theorem linear_map.smul_comp
deleted theorem linear_map.sub_apply
deleted theorem linear_map.sub_comp
deleted theorem linear_map.zero_apply
deleted theorem linear_map.zero_comp