Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2019-09-24 00:00 425644f8

View on Github →

refactor(algebra/*): Make monoid_hom.ext etc use ∀ x, f x = g x as an assumption (#1476)

Estimated changes

added theorem monoid_hom.coe_inj
modified theorem monoid_hom.ext
added theorem monoid_hom.ext_iff
added theorem ring_hom.coe_inj
modified theorem ring_hom.ext
added theorem ring_hom.ext_iff