Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2022-05-17 13:06 65bf1349

View on Github →

split(algebra/hom/ring): Split off algebra.ring.basic (#14144) Move non_unital_ring_hom and ring_hom to a new file algebra.hom.ring. Crediting

Estimated changes

added theorem map_bit1
added structure non_unital_ring_hom
added theorem ring_hom.cancel_left
added theorem ring_hom.cancel_right
added theorem ring_hom.coe_coe
added theorem ring_hom.coe_comp
added theorem ring_hom.coe_inj
added theorem ring_hom.coe_mk
added theorem ring_hom.coe_mul
added theorem ring_hom.coe_one
added def ring_hom.comp
added theorem ring_hom.comp_apply
added theorem ring_hom.comp_assoc
added theorem ring_hom.comp_id
added theorem ring_hom.congr_arg
added theorem ring_hom.congr_fun
added def ring_hom.copy
added theorem ring_hom.ext
added theorem ring_hom.ext_iff
added def ring_hom.id
added theorem ring_hom.id_apply
added theorem ring_hom.id_comp
added theorem ring_hom.is_unit_map
added def ring_hom.mk'
added theorem ring_hom.mk_coe
added theorem ring_hom.mul_def
added theorem ring_hom.one_def
added theorem ring_hom.to_fun_eq_coe
added structure ring_hom
deleted theorem map_bit1
deleted theorem non_unital_ring_hom.ext
deleted structure non_unital_ring_hom
deleted theorem ring_hom.cancel_left
deleted theorem ring_hom.cancel_right
deleted theorem ring_hom.coe_coe
deleted theorem ring_hom.coe_comp
deleted theorem ring_hom.coe_inj
deleted theorem ring_hom.coe_mk
deleted theorem ring_hom.coe_monoid_hom
deleted theorem ring_hom.coe_mul
deleted theorem ring_hom.coe_one
deleted def ring_hom.comp
deleted theorem ring_hom.comp_apply
deleted theorem ring_hom.comp_assoc
deleted theorem ring_hom.comp_id
deleted theorem ring_hom.congr_arg
deleted theorem ring_hom.congr_fun
deleted def ring_hom.copy
deleted theorem ring_hom.ext
deleted theorem ring_hom.ext_iff
deleted def ring_hom.id
deleted theorem ring_hom.id_apply
deleted theorem ring_hom.id_comp
deleted theorem ring_hom.is_unit_map
deleted theorem ring_hom.map_dvd
deleted theorem ring_hom.map_one_ne_zero
deleted def ring_hom.mk'
deleted theorem ring_hom.mk_coe
deleted theorem ring_hom.mul_def
deleted theorem ring_hom.one_def
deleted theorem ring_hom.to_fun_eq_coe
deleted structure ring_hom
modified theorem two_dvd_bit0