Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2022-12-09 09:32 b16045e4

View on Github →

refactor(algebra/algebra): split alg_hom and alg_equiv to separate files (#17868) The motivation here is mainly to make the file shorter.

Estimated changes

deleted def alg_equiv.aut_congr
deleted theorem alg_equiv.aut_congr_refl
deleted theorem alg_equiv.aut_congr_symm
deleted theorem alg_equiv.aut_congr_trans
deleted theorem alg_equiv.coe_alg_hom
deleted theorem alg_equiv.coe_coe
deleted theorem alg_equiv.coe_mk
deleted theorem alg_equiv.coe_refl
deleted theorem alg_equiv.coe_ring_equiv'
deleted theorem alg_equiv.coe_ring_equiv
deleted theorem alg_equiv.coe_trans
deleted theorem alg_equiv.commutes
deleted theorem alg_equiv.comp_symm
deleted theorem alg_equiv.ext
deleted theorem alg_equiv.inv_fun_eq_symm
deleted theorem alg_equiv.map_finsupp_sum
deleted theorem alg_equiv.map_prod
deleted theorem alg_equiv.map_smul
deleted theorem alg_equiv.map_sum
deleted theorem alg_equiv.mk_coe'
deleted theorem alg_equiv.mk_coe
deleted theorem alg_equiv.mul_apply
deleted theorem alg_equiv.of_alg_hom_symm
deleted theorem alg_equiv.one_apply
deleted def alg_equiv.refl
deleted theorem alg_equiv.refl_symm
deleted theorem alg_equiv.refl_to_alg_hom
deleted def alg_equiv.symm
deleted theorem alg_equiv.symm_bijective
deleted theorem alg_equiv.symm_comp
deleted theorem alg_equiv.symm_mk
deleted theorem alg_equiv.symm_symm
deleted theorem alg_equiv.to_equiv_eq_coe
deleted theorem alg_equiv.to_fun_eq_coe
deleted def alg_equiv.trans
deleted theorem alg_equiv.trans_apply
deleted structure alg_equiv
deleted theorem alg_hom.coe_coe
deleted theorem alg_hom.coe_comp
deleted theorem alg_hom.coe_fn_inj
deleted theorem alg_hom.coe_fn_injective
deleted theorem alg_hom.coe_id
deleted theorem alg_hom.coe_mk'
deleted theorem alg_hom.coe_mk
deleted theorem alg_hom.coe_to_monoid_hom
deleted theorem alg_hom.coe_to_ring_hom
deleted theorem alg_hom.commutes
deleted def alg_hom.comp
deleted theorem alg_hom.comp_algebra_map
deleted theorem alg_hom.comp_apply
deleted theorem alg_hom.comp_assoc
deleted theorem alg_hom.comp_id
deleted theorem alg_hom.comp_to_ring_hom
deleted theorem alg_hom.ext
deleted theorem alg_hom.ext_iff
deleted theorem alg_hom.id_apply
deleted theorem alg_hom.id_comp
deleted theorem alg_hom.id_to_ring_hom
deleted theorem alg_hom.map_list_prod
deleted theorem alg_hom.map_smul_of_tower
deleted def alg_hom.mk'
deleted theorem alg_hom.mk_coe
deleted theorem alg_hom.mul_apply
deleted theorem alg_hom.of_linear_map_id
deleted theorem alg_hom.one_apply
deleted theorem alg_hom.to_fun_eq_coe
deleted theorem alg_hom.to_linear_map_id
deleted structure alg_hom
deleted def algebra.of_id
deleted theorem algebra.of_id_apply
added theorem alg_equiv.coe_alg_hom
added theorem alg_equiv.coe_coe
added theorem alg_equiv.coe_mk
added theorem alg_equiv.coe_refl
added theorem alg_equiv.coe_trans
added theorem alg_equiv.commutes
added theorem alg_equiv.comp_symm
added theorem alg_equiv.ext
added theorem alg_equiv.map_prod
added theorem alg_equiv.map_smul
added theorem alg_equiv.map_sum
added theorem alg_equiv.mk_coe'
added theorem alg_equiv.mk_coe
added theorem alg_equiv.mul_apply
added theorem alg_equiv.one_apply
added def alg_equiv.refl
added theorem alg_equiv.refl_symm
added def alg_equiv.symm
added theorem alg_equiv.symm_comp
added theorem alg_equiv.symm_mk
added theorem alg_equiv.symm_symm
added def alg_equiv.trans
added theorem alg_equiv.trans_apply
added structure alg_equiv
added theorem alg_hom.coe_coe
added theorem alg_hom.coe_comp
added theorem alg_hom.coe_fn_inj
added theorem alg_hom.coe_id
added theorem alg_hom.coe_mk'
added theorem alg_hom.coe_mk
added theorem alg_hom.commutes
added def alg_hom.comp
added theorem alg_hom.comp_apply
added theorem alg_hom.comp_assoc
added theorem alg_hom.comp_id
added theorem alg_hom.ext
added theorem alg_hom.ext_iff
added theorem alg_hom.id_apply
added theorem alg_hom.id_comp
added theorem alg_hom.id_to_ring_hom
added theorem alg_hom.map_list_prod
added def alg_hom.mk'
added theorem alg_hom.mk_coe
added theorem alg_hom.mul_apply
added theorem alg_hom.one_apply
added theorem alg_hom.to_fun_eq_coe
added structure alg_hom
added def algebra.of_id
added theorem algebra.of_id_apply