Commit 2025-01-15 21:51 42d20c7e

View on Github →

chore(Algebra/Group/Equiv): split into Defs and Basic (#20712) While looking at the import graph for Mathlib.Data.NNRat.Defs, I noticed that there isn't a Defs file for group equivs, while there is one for linear equivs. With this PR, the design of Algebra/Group/Equiv matches Algebra/Module/Equiv better.

Estimated changes

deleted structure AddEquiv
deleted theorem MulEquiv.apply_eq_iff_eq
deleted theorem MulEquiv.apply_symm_apply
deleted theorem MulEquiv.coe_mk
deleted theorem MulEquiv.coe_refl
deleted theorem MulEquiv.coe_toEquiv
deleted theorem MulEquiv.coe_toEquiv_symm
deleted theorem MulEquiv.coe_toMonoidHom
deleted theorem MulEquiv.coe_toMulHom
deleted theorem MulEquiv.coe_trans
deleted theorem MulEquiv.comp_symm_eq
deleted theorem MulEquiv.eq_comp_symm
deleted theorem MulEquiv.eq_symm_apply
deleted theorem MulEquiv.eq_symm_comp
deleted theorem MulEquiv.ext
deleted theorem MulEquiv.invFun_eq_symm
deleted theorem MulEquiv.map_ne_one_iff
deleted def MulEquiv.mk'
deleted theorem MulEquiv.mk_coe'
deleted theorem MulEquiv.mk_coe
deleted def MulEquiv.refl
deleted theorem MulEquiv.refl_apply
deleted theorem MulEquiv.refl_symm
deleted theorem MulEquiv.self_comp_symm
deleted theorem MulEquiv.self_trans_symm
deleted def MulEquiv.symm
deleted theorem MulEquiv.symm_apply_apply
deleted theorem MulEquiv.symm_apply_eq
deleted theorem MulEquiv.symm_bijective
deleted theorem MulEquiv.symm_comp_eq
deleted theorem MulEquiv.symm_comp_self
deleted theorem MulEquiv.symm_map_mul
deleted theorem MulEquiv.symm_mk
deleted theorem MulEquiv.symm_symm
deleted theorem MulEquiv.symm_trans_apply
deleted theorem MulEquiv.symm_trans_self
deleted theorem MulEquiv.toEquiv_eq_coe
deleted theorem MulEquiv.toEquiv_symm
deleted theorem MulEquiv.toFun_eq_coe
deleted theorem MulEquiv.toMulHom_eq_coe
deleted def MulEquiv.trans
deleted theorem MulEquiv.trans_apply
deleted structure MulEquiv
deleted def MulHom.toMulEquiv
added structure AddEquiv
added theorem MulEquiv.coe_mk
added theorem MulEquiv.coe_refl
added theorem MulEquiv.coe_toEquiv
added theorem MulEquiv.coe_toMulHom
added theorem MulEquiv.coe_trans
added theorem MulEquiv.comp_symm_eq
added theorem MulEquiv.eq_comp_symm
added theorem MulEquiv.eq_symm_apply
added theorem MulEquiv.eq_symm_comp
added theorem MulEquiv.ext
added def MulEquiv.mk'
added theorem MulEquiv.mk_coe'
added theorem MulEquiv.mk_coe
added def MulEquiv.refl
added theorem MulEquiv.refl_apply
added theorem MulEquiv.refl_symm
added def MulEquiv.symm
added theorem MulEquiv.symm_apply_eq
added theorem MulEquiv.symm_comp_eq
added theorem MulEquiv.symm_map_mul
added theorem MulEquiv.symm_mk
added theorem MulEquiv.symm_symm
added theorem MulEquiv.toEquiv_symm
added theorem MulEquiv.toFun_eq_coe
added def MulEquiv.trans
added theorem MulEquiv.trans_apply
added structure MulEquiv