Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2021-09-24 19:49 7cb72461

View on Github →

chore(linear_algebra/basic): add linear_map.neg_comp, generalize linear_map.{sub,smul}_comp (#9335) sub_comp had unnecessary requirements that the codomain of the right map be an additive group, while smul_comp did not support compatible actions. This also golfs the proofs of all the comp_* lemmas to eliminate simp. smul_comp and comp_smul are also both promoted to instances.

Estimated changes

modified theorem linear_map.add_comp
modified theorem linear_map.comp_add
modified theorem linear_map.comp_neg
modified theorem linear_map.comp_smul
modified theorem linear_map.comp_sub
modified theorem linear_map.neg_apply
added theorem linear_map.neg_comp
modified theorem linear_map.sub_apply
modified theorem linear_map.sub_comp