Commit 2024-11-21 09:25 e4a142c2

View on Github →

chore(Algebra/Group/Subgroup): split Lattice, Map, Ker from Basic.lean (#19295) The file Algebra/Group/Subgroup/Basic.lean is very long. Following the design of the Submodule folder, split it into:

  • Lattice.lean: CompleteLattice instance, Subgroup.closure
  • Map.lean: Subgroup.map, Subgroup.comap
  • Ker.lean: MonoidHom.ker, MonoidHom.range and MonoidHom.eqLocus

Estimated changes

deleted theorem MonoidHom.coe_ker
deleted theorem MonoidHom.coe_range
deleted theorem MonoidHom.comap_bot
deleted theorem MonoidHom.comap_ker
deleted theorem MonoidHom.div_mem_ker_iff
deleted def MonoidHom.eqLocus
deleted theorem MonoidHom.eqLocus_same
deleted theorem MonoidHom.eqOn_closure
deleted theorem MonoidHom.eq_iff
deleted theorem MonoidHom.eq_of_eqOn_top
deleted def MonoidHom.ker
deleted theorem MonoidHom.ker_codRestrict
deleted theorem MonoidHom.ker_eq_bot_iff
deleted theorem MonoidHom.ker_id
deleted theorem MonoidHom.ker_one
deleted theorem MonoidHom.ker_prod
deleted theorem MonoidHom.ker_restrict
deleted theorem MonoidHom.ker_toHomUnits
deleted theorem MonoidHom.map_closure
deleted theorem MonoidHom.map_range
deleted theorem MonoidHom.mem_ker
deleted theorem MonoidHom.mem_range
deleted def MonoidHom.range
deleted theorem MonoidHom.range_eq_map
deleted theorem MonoidHom.range_eq_top
deleted theorem MonoidHom.range_one
deleted theorem MonoidHom.restrict_range
deleted theorem Subgroup.bot_subgroupOf
deleted theorem Subgroup.bot_toSubmonoid
deleted def Subgroup.closure
deleted theorem Subgroup.closure_empty
deleted theorem Subgroup.closure_eq
deleted theorem Subgroup.closure_eq_of_le
deleted theorem Subgroup.closure_iUnion
deleted theorem Subgroup.closure_le
deleted theorem Subgroup.closure_mono
deleted theorem Subgroup.closure_union
deleted theorem Subgroup.closure_univ
deleted theorem Subgroup.coe_bot
deleted theorem Subgroup.coe_comap
deleted theorem Subgroup.coe_eq_singleton
deleted theorem Subgroup.coe_eq_univ
deleted theorem Subgroup.coe_iInf
deleted theorem Subgroup.coe_inf
deleted theorem Subgroup.coe_map
deleted theorem Subgroup.coe_sInf
deleted theorem Subgroup.coe_subgroupOf
deleted theorem Subgroup.coe_top
deleted def Subgroup.comap
deleted theorem Subgroup.comap_comap
deleted theorem Subgroup.comap_iInf
deleted theorem Subgroup.comap_id
deleted theorem Subgroup.comap_inf
deleted theorem Subgroup.comap_injective
deleted theorem Subgroup.comap_map_eq
deleted theorem Subgroup.comap_mono
deleted theorem Subgroup.comap_subtype
deleted theorem Subgroup.comap_sup_eq
deleted theorem Subgroup.comap_top
deleted theorem Subgroup.disjoint_def'
deleted theorem Subgroup.disjoint_def
deleted theorem Subgroup.eq_top_iff'
deleted theorem Subgroup.gc_map_comap
deleted theorem Subgroup.iSup_comap_le
deleted theorem Subgroup.iSup_eq_closure
deleted theorem Subgroup.inclusion_range
deleted theorem Subgroup.ker_inclusion
deleted theorem Subgroup.ker_le_comap
deleted theorem Subgroup.ker_subtype
deleted theorem Subgroup.le_comap_map
deleted def Subgroup.map
deleted theorem Subgroup.map_bot
deleted theorem Subgroup.map_comap_eq
deleted theorem Subgroup.map_comap_le
deleted theorem Subgroup.map_eq_bot_iff
deleted theorem Subgroup.map_eq_map_iff
deleted theorem Subgroup.map_eq_range_iff
deleted theorem Subgroup.map_iInf
deleted theorem Subgroup.map_iSup
deleted theorem Subgroup.map_id
deleted theorem Subgroup.map_inf
deleted theorem Subgroup.map_inf_eq
deleted theorem Subgroup.map_inf_le
deleted theorem Subgroup.map_injective
deleted theorem Subgroup.map_le_map_iff'
deleted theorem Subgroup.map_le_map_iff
deleted theorem Subgroup.map_le_range
deleted theorem Subgroup.map_map
deleted theorem Subgroup.map_mono
deleted theorem Subgroup.map_one_eq_bot
deleted theorem Subgroup.map_subtype_le
deleted theorem Subgroup.map_sup
deleted theorem Subgroup.mem_bot
deleted theorem Subgroup.mem_closure
deleted theorem Subgroup.mem_closure_pair
deleted theorem Subgroup.mem_comap
deleted theorem Subgroup.mem_iInf
deleted theorem Subgroup.mem_iSup_of_mem
deleted theorem Subgroup.mem_inf
deleted theorem Subgroup.mem_map
deleted theorem Subgroup.mem_map_equiv
deleted theorem Subgroup.mem_map_iff_mem
deleted theorem Subgroup.mem_map_of_mem
deleted theorem Subgroup.mem_sInf
deleted theorem Subgroup.mem_sSup_of_mem
deleted theorem Subgroup.mem_subgroupOf
deleted theorem Subgroup.mem_sup'
deleted theorem Subgroup.mem_sup
deleted theorem Subgroup.mem_sup_left
deleted theorem Subgroup.mem_sup_right
deleted theorem Subgroup.mem_top
deleted theorem Subgroup.mul_mem_sup
deleted theorem Subgroup.nontrivial_iff
deleted def Subgroup.subgroupOf
deleted theorem Subgroup.subgroupOf_inj
deleted theorem Subgroup.subgroupOf_self
deleted theorem Subgroup.subgroupOf_sup
deleted theorem Subgroup.subset_closure
deleted theorem Subgroup.subsingleton_iff
deleted theorem Subgroup.subtype_range
deleted theorem Subgroup.sup_eq_closure
deleted def Subgroup.topEquiv
deleted theorem Subgroup.top_subgroupOf
deleted theorem Subgroup.top_toSubmonoid
added theorem MonoidHom.coe_ker
added theorem MonoidHom.coe_range
added theorem MonoidHom.comap_bot
added theorem MonoidHom.comap_ker
added theorem MonoidHom.eqLocus_same
added theorem MonoidHom.eqOn_closure
added theorem MonoidHom.eq_iff
added def MonoidHom.ker
added theorem MonoidHom.ker_id
added theorem MonoidHom.ker_one
added theorem MonoidHom.ker_prod
added theorem MonoidHom.ker_restrict
added theorem MonoidHom.map_range
added theorem MonoidHom.mem_ker
added theorem MonoidHom.mem_range
added def MonoidHom.range
added theorem MonoidHom.range_eq_map
added theorem MonoidHom.range_eq_top
added theorem MonoidHom.range_one
added theorem Subgroup.comap_map_eq
added theorem Subgroup.comap_sup_eq
added theorem Subgroup.ker_inclusion
added theorem Subgroup.ker_le_comap
added theorem Subgroup.ker_subtype
added theorem Subgroup.map_comap_eq
added theorem Subgroup.map_injective
added theorem Subgroup.map_le_range
added theorem Subgroup.subtype_range
added def Subgroup.closure
added theorem Subgroup.closure_empty
added theorem Subgroup.closure_eq
added theorem Subgroup.closure_le
added theorem Subgroup.closure_mono
added theorem Subgroup.closure_union
added theorem Subgroup.closure_univ
added theorem Subgroup.coe_bot
added theorem Subgroup.coe_eq_univ
added theorem Subgroup.coe_iInf
added theorem Subgroup.coe_inf
added theorem Subgroup.coe_sInf
added theorem Subgroup.coe_top
added theorem Subgroup.disjoint_def'
added theorem Subgroup.disjoint_def
added theorem Subgroup.eq_top_iff'
added theorem Subgroup.mem_bot
added theorem Subgroup.mem_closure
added theorem Subgroup.mem_iInf
added theorem Subgroup.mem_inf
added theorem Subgroup.mem_sInf
added theorem Subgroup.mem_sup'
added theorem Subgroup.mem_sup
added theorem Subgroup.mem_sup_left
added theorem Subgroup.mem_sup_right
added theorem Subgroup.mem_top
added theorem Subgroup.mul_mem_sup
added theorem MonoidHom.map_closure
added theorem Subgroup.coe_comap
added theorem Subgroup.coe_map
added def Subgroup.comap
added theorem Subgroup.comap_comap
added theorem Subgroup.comap_iInf
added theorem Subgroup.comap_id
added theorem Subgroup.comap_inf
added theorem Subgroup.comap_mono
added theorem Subgroup.comap_subtype
added theorem Subgroup.comap_top
added theorem Subgroup.gc_map_comap
added theorem Subgroup.iSup_comap_le
added theorem Subgroup.le_comap_map
added def Subgroup.map
added theorem Subgroup.map_bot
added theorem Subgroup.map_comap_le
added theorem Subgroup.map_iInf
added theorem Subgroup.map_iSup
added theorem Subgroup.map_id
added theorem Subgroup.map_inf
added theorem Subgroup.map_inf_eq
added theorem Subgroup.map_inf_le
added theorem Subgroup.map_map
added theorem Subgroup.map_mono
added theorem Subgroup.map_sup
added theorem Subgroup.mem_comap
added theorem Subgroup.mem_map
added theorem Subgroup.mem_map_equiv