Commit 2020-10-13 14:02 ca6af1c4

View on Github →

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.

Estimated changes

Modified src/algebra/monoid_algebra.lean

deleted def add_monoid_algebra.algebra_map'

added def add_monoid_algebra.single_zero_alg_hom

added def add_monoid_algebra.single_zero_ring_hom

deleted def monoid_algebra.algebra_map'

added def monoid_algebra.single_one_alg_hom

added def monoid_algebra.single_one_ring_hom

Modified src/data/polynomial/monomial.lean

modified def polynomial.C