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.