Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2020-05-11 06:32 ff37fb8a

View on Github →

feat(algebra/ring): monoid structure on R →+* R (#2649) Also add comp_id and id_comp

Estimated changes

added theorem ring_hom.coe_pow
added theorem ring_hom.coe_mul
added theorem ring_hom.coe_one
added theorem ring_hom.comp_id
added theorem ring_hom.id_comp
modified def ring_hom.mk'
added theorem ring_hom.mul_def
added theorem ring_hom.one_def