Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2022-03-02 22:17 6f74d3cc

View on Github →

chore(algebra/ring/basic): generalize lemmas to non-associative rings (#12411)

Estimated changes

modified theorem ring_hom.injective_iff'
modified theorem ring_hom.injective_iff
modified def ring_hom.mk'