linear_map): Derive linear_map from mul_action_hom (#4888)

Commit

5 years ago

chore(algebra/module/linear_map): Derive linear_map from mul_action_hom (#4888) Note that this required some stuff about polynomials to move to cut import cycles.

References

#4925 - Make prime-avoidance branch build

Author

eric-wieser

Parents

2f07ff21

mathlib 6a1ce57b - chore(algebra/module/linear_map): Derive linear_map from mul_action_hom (#4888)

mathlib
6a1ce57b - chore(algebra/module/linear_map): Derive linear_map from mul_action_hom (#4888)