Commit 2022-12-13 11:06 2e890fb3

View on Github →

feat: Port Algebra.Hom.Ring (#958) mathlib3 SHA: cf9386b56953fb40904843af98b7a80757bbe7f9

Estimated changes

added theorem NonUnitalRingHom.ext
added structure NonUnitalRingHom
added theorem RingHom.cancel_left
added theorem RingHom.cancel_right
added theorem RingHom.coe_coe
added theorem RingHom.coe_comp
added theorem RingHom.coe_copy
added theorem RingHom.coe_inj
added theorem RingHom.coe_mk
added theorem RingHom.coe_mul
added theorem RingHom.coe_one
added def RingHom.comp
added theorem RingHom.comp_apply
added theorem RingHom.comp_assoc
added theorem RingHom.comp_id
added theorem RingHom.congr_arg
added theorem RingHom.congr_fun
added def RingHom.copy
added theorem RingHom.copy_eq
added theorem RingHom.ext
added theorem RingHom.ext_iff
added def RingHom.id
added theorem RingHom.id_apply
added theorem RingHom.id_comp
added theorem RingHom.is_unit_map
added def RingHom.mk'
added theorem RingHom.mk_coe
added theorem RingHom.mul_def
added theorem RingHom.one_def
added theorem RingHom.toFun_eq_coe
added structure RingHom