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.