Commit 2023-01-17 13:16 2bc4fedb

View on Github →

feat: port GroupTheory/Congruence (#1316) wip

Estimated changes

Modified Mathlib.lean

Created Mathlib/GroupTheory/Congruence.lean

added structure AddCon

added inductive AddConGen.Rel

added theorem Con.coe_mk'

added theorem Con.coe_mul

added theorem Con.coe_one

added theorem Con.coe_smul

added def Con.comap

added theorem Con.comap_eq

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 def Con.correspondence

added theorem Con.ext'

added theorem Con.ext'_iff

added theorem Con.ext

added theorem Con.ext_iff

added theorem Con.hrec_on₂_coe

added theorem Con.induction_on_units

added theorem Con.inf_def

added theorem Con.inf_iff_and

added theorem Con.infₛ_def

added theorem Con.infₛ_toSetoid

added def Con.ker

added def Con.kerLift

added theorem Con.kerLift_injective

added theorem Con.kerLift_mk

added theorem Con.kerLift_range_eq

added theorem Con.ker_apply_eq_preimage

added theorem Con.ker_eq_lift_of_injective

added theorem Con.ker_rel

added theorem Con.le_def

added theorem Con.le_iff

added def Con.lift

added def Con.liftOnUnits

added theorem Con.liftOnUnits_mk

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_range

added theorem Con.lift_surjective_of_surjective

added theorem Con.lift_unique

added def Con.map

added def Con.mapGen

added def Con.mapOfSurjective

added theorem Con.mapOfSurjective_eq_mapGen

added theorem Con.map_apply

added theorem Con.mem_coe

added def Con.mk'

added theorem Con.mk'_ker

added theorem Con.mk'_surjective

added theorem Con.mrange_mk'

added def Con.mulKer

added theorem Con.mul_ker_mk_eq

added def Con.ofSubmonoid

added def Con.pi

added theorem Con.quot_mk_eq_coe

added def Con.quotientKerEquivOfRightInverse

added def Con.quotientQuotientEquivQuotient

added theorem Con.rel_eq_coe

added theorem Con.rel_mk

added theorem Con.smul

added theorem Con.sup_def

added theorem Con.sup_eq_conGen

added theorem Con.supₛ_def

added theorem Con.supₛ_eq_conGen

added def Con.toQuotient

added theorem Con.toSetoid_inj

added theorem Con.to_submonoid_inj

added structure Con

added inductive ConGen.Rel

added def conGen