Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2020-06-04 16:18 1a297969

View on Github →

chore(is_ring_hom): remove some uses of is_ring_hom (#2884) This PR deletes the definitions is_ring_anti_hom and ring_anti_equiv, in favour of using the bundled R →+* Rᵒᵖ and R ≃+* Rᵒᵖ. It also changes the definition of ring_invo. This is work towards removing the deprecated is_*_hom family.

Estimated changes

added theorem opposite.op_eq_one_iff
added theorem mul_equiv.to_fun_apply
modified theorem sesq_form.neg_left
modified theorem sesq_form.neg_right
modified theorem sesq_form.smul_right
modified theorem sesq_form.zero_left
modified theorem sesq_form.zero_right
modified structure sesq_form
modified theorem sym_sesq_form.is_refl
modified def sym_sesq_form.is_sym
modified theorem sym_sesq_form.sym
deleted theorem comm_ring.anti_hom_to_hom
deleted theorem comm_ring.hom_to_anti_hom
deleted theorem is_ring_anti_hom.map_neg
deleted theorem is_ring_anti_hom.map_sub
deleted theorem is_ring_anti_hom.map_zero
deleted theorem ring_anti_equiv.bijective
deleted theorem ring_anti_equiv.map_add
deleted theorem ring_anti_equiv.map_mul
deleted theorem ring_anti_equiv.map_neg
deleted theorem ring_anti_equiv.map_one
deleted theorem ring_anti_equiv.map_sub
deleted theorem ring_anti_equiv.map_zero
deleted structure ring_anti_equiv
deleted theorem ring_equiv.bijective
deleted theorem ring_equiv.map_zero_iff
deleted theorem ring_invo.bijective
deleted theorem ring_invo.map_add
deleted theorem ring_invo.map_mul
deleted theorem ring_invo.map_neg
deleted theorem ring_invo.map_neg_one
deleted theorem ring_invo.map_one
deleted theorem ring_invo.map_sub
deleted theorem ring_invo.map_zero
deleted theorem ring_invo.map_zero_iff
added def ring_invo.mk'
modified structure ring_invo