Commit 2022-09-13 04:22 5bd4f627
View on Github →chore(ring_theory/local_properties): remove coercions from ring_hom to monoid_hom (#16453)
Now that submonoid.map takes monoid_hom_class, these aren't necessary. Also golfs a pair of proofs.
chore(ring_theory/local_properties): remove coercions from ring_hom to monoid_hom (#16453)
Now that submonoid.map takes monoid_hom_class, these aren't necessary. Also golfs a pair of proofs.