mathlib

5bd4f627 - chore(ring_theory/local_properties): remove coercions from `ring_hom` to `monoid_hom` (#16453)

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.