Commit 2021-08-31 21:31 93390069

feat(algebra/{module/linear_map, algebra/basic}): Add distrib_mul_action.to_linear_(map|equiv) and mul_semiring_action.to_alg_(hom|equiv) (#8936) This adds the following stronger versions of distrib_mul_action.to_add_monoid_hom:

• distrib_mul_action.to_linear_map
• distrib_mul_action.to_linear_equiv
• mul_semiring_action.to_alg_hom
• mul_semiring_action.to_alg_equiv Zulip thread