mathlib3
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)

Commit
4 years ago
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](https://leanprover.zulipchat.com/#narrow/stream/217875-Is-there.20code.20for.20X.3F/topic/group.20acting.20on.20algebra/near/251372497)
Author
Parents
Loading