Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2020-10-08 15:41 60be8ed5

View on Github →

feat(data/equiv/*): to_monoid_hom_injective and to_ring_hom_injective (#4525)

Estimated changes

Modified src/data/equiv/mul_add.lean

added theorem mul_equiv.to_monoid_hom_injective

Modified src/data/equiv/ring.lean

added theorem ring_equiv.to_ring_hom_injective