Commit 2024-10-15 03:55 9958ee4c

View on Github →

chore(GroupTheory/Congruence/Basic): split off Defs and Hom (#17729) GroupTheory.Congruence.Defs sets up the quotient and its monoid structure, and its imports and contents are trimmed down to the minimum to make that possible. GroupTheory.Congruence.Hom are those results that couldn't go into GroupTheory.Congruence.Defs but can be added after we import monoid homs.

Estimated changes

deleted structure AddCon
deleted inductive AddConGen.Rel
deleted theorem Con.coe_iInf
deleted theorem Con.coe_inf
deleted theorem Con.coe_inj
deleted theorem Con.coe_mk'
deleted theorem Con.coe_mul
deleted theorem Con.coe_one
deleted theorem Con.coe_sInf
deleted def Con.comap
deleted theorem Con.comap_eq
deleted theorem Con.comap_rel
deleted theorem Con.conGen_eq
deleted theorem Con.conGen_idem
deleted theorem Con.conGen_le
deleted theorem Con.conGen_mono
deleted theorem Con.conGen_of_con
deleted def Con.correspondence
deleted theorem Con.ext'
deleted theorem Con.ext
deleted theorem Con.hrec_on₂_coe
deleted theorem Con.induction_on_units
deleted theorem Con.inf_iff_and
deleted def Con.ker
deleted def Con.kerLift
deleted theorem Con.kerLift_injective
deleted theorem Con.kerLift_mk
deleted theorem Con.ker_apply
deleted theorem Con.ker_rel
deleted theorem Con.le_def
deleted def Con.lift
deleted def Con.liftOnUnits
deleted theorem Con.liftOnUnits_mk
deleted theorem Con.lift_apply_mk'
deleted theorem Con.lift_coe
deleted theorem Con.lift_comp_mk'
deleted theorem Con.lift_funext
deleted theorem Con.lift_mk'
deleted theorem Con.lift_unique
deleted def Con.map
deleted def Con.mapGen
deleted def Con.mapOfSurjective
deleted theorem Con.map_apply
deleted def Con.mk'
deleted theorem Con.mk'_ker
deleted theorem Con.mk'_surjective
deleted def Con.mulKer
deleted theorem Con.mul_ker_mk_eq
deleted theorem Con.quot_mk_eq_coe
deleted theorem Con.rel_eq_coe
deleted theorem Con.rel_mk
deleted theorem Con.sInf_toSetoid
deleted theorem Con.sSup_def
deleted theorem Con.sSup_eq_conGen
deleted theorem Con.sup_def
deleted theorem Con.sup_eq_conGen
deleted def Con.toQuotient
deleted theorem Con.toSetoid_inj
deleted structure Con
deleted inductive ConGen.Rel
deleted def conGen
added structure AddCon
added inductive AddConGen.Rel
added theorem Con.coe_iInf
added theorem Con.coe_inf
added theorem Con.coe_inj
added theorem Con.coe_mul
added theorem Con.coe_one
added theorem Con.coe_sInf
added def Con.comap
added theorem Con.comap_rel
added theorem Con.conGen_eq
added theorem Con.conGen_idem
added theorem Con.conGen_le
added theorem Con.conGen_mono
added theorem Con.conGen_of_con
added theorem Con.ext'
added theorem Con.ext
added theorem Con.hrec_on₂_coe
added theorem Con.induction_on_units
added theorem Con.inf_iff_and
added theorem Con.le_def
added def Con.liftOnUnits
added theorem Con.liftOnUnits_mk
added def Con.mapGen
added def Con.mulKer
added theorem Con.mul_ker_mk_eq
added theorem Con.quot_mk_eq_coe
added theorem Con.rel_eq_coe
added theorem Con.rel_mk
added theorem Con.sInf_toSetoid
added theorem Con.sSup_def
added theorem Con.sSup_eq_conGen
added theorem Con.sup_def
added theorem Con.sup_eq_conGen
added def Con.toQuotient
added theorem Con.toSetoid_inj
added structure Con
added inductive ConGen.Rel
added def conGen
added theorem Con.coe_mk'
added theorem Con.comap_eq
added def Con.ker
added def Con.kerLift
added theorem Con.kerLift_injective
added theorem Con.kerLift_mk
added theorem Con.ker_apply
added theorem Con.ker_rel
added def Con.lift
added theorem Con.lift_apply_mk'
added theorem Con.lift_coe
added theorem Con.lift_comp_mk'
added theorem Con.lift_funext
added theorem Con.lift_mk'
added theorem Con.lift_unique
added def Con.map
added theorem Con.map_apply
added def Con.mk'
added theorem Con.mk'_ker
added theorem Con.mk'_surjective