mathlib3
ca6af1c4 - chore(algebra/monoid_algebra): Replace `algebra_map'` with `single_(zero|one)_ring_hom` (#4582)

Commit
5 years ago
chore(algebra/monoid_algebra): Replace `algebra_map'` with `single_(zero|one)_ring_hom` (#4582) `algebra_map'` is now trivially equal to `single_(zero|one)_ring_hom.comp`, so is no longer needed.
Author
Parents
Loading