Mathlib v3 is deprecated. Go to Mathlib v4

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.

Estimated changes