Commit 2023-01-26 10:26 746cf5ab

View on Github →

feat: port GroupTheory.Subgroup.Basic (#1797)

Estimated changes

Modified Mathlib.lean

Created Mathlib/GroupTheory/Subgroup/Basic.lean

added structure AddSubgroup.Characteristic

added structure AddSubgroup.IsCommutative

added structure AddSubgroup.Normal

added def AddSubgroup.toSubgroup

added structure AddSubgroup

added theorem CommGroup.center_eq_top

added def Group.commGroupOfCenterEqTop

added theorem Group.conj_mem_conjugatesOfSet

added def Group.conjugatesOfSet

added theorem Group.conjugatesOfSet_mono

added theorem Group.conjugatesOfSet_subset

added theorem Group.conjugates_subset_normal

added theorem Group.mem_conjugatesOfSet_iff

added theorem Group.subset_conjugatesOfSet

added theorem IsConj.normalClosure_eq_top_of

added theorem MonoidHom.closure_preimage_le

added theorem MonoidHom.coe_comp_rangeRestrict

added theorem MonoidHom.coe_ker

added theorem MonoidHom.coe_range

added theorem MonoidHom.coe_rangeRestrict

added theorem MonoidHom.comap_bot

added theorem MonoidHom.comap_ker

added def MonoidHom.eqLocus

added theorem MonoidHom.eqLocus_same

added theorem MonoidHom.eqOn_closure

added theorem MonoidHom.eq_iff

added theorem MonoidHom.eq_liftOfRightInverse

added theorem MonoidHom.eq_of_eqOn_dense

added theorem MonoidHom.eq_of_eqOn_top

added def MonoidHom.ker

added theorem MonoidHom.ker_codRestrict

added theorem MonoidHom.ker_eq_bot_iff

added theorem MonoidHom.ker_id

added theorem MonoidHom.ker_one

added theorem MonoidHom.ker_prodMap

added theorem MonoidHom.ker_rangeRestrict

added theorem MonoidHom.ker_restrict

added theorem MonoidHom.ker_toHomUnits

added def MonoidHom.liftOfRightInverse

added def MonoidHom.liftOfRightInverseAux

added theorem MonoidHom.liftOfRightInverseAux_comp_apply

added theorem MonoidHom.liftOfRightInverse_comp

added theorem MonoidHom.liftOfRightInverse_comp_apply

added theorem MonoidHom.map_closure

added theorem MonoidHom.map_range

added theorem MonoidHom.mem_ker

added theorem MonoidHom.mem_range

added theorem MonoidHom.ofInjective_apply

added def MonoidHom.ofLeftInverse

added theorem MonoidHom.ofLeftInverse_apply

added theorem MonoidHom.ofLeftInverse_symm_apply

added theorem MonoidHom.prodMap_comap_prod

added def MonoidHom.range

added def MonoidHom.rangeRestrict

added theorem MonoidHom.rangeRestrict_surjective

added theorem MonoidHom.range_eq_map

added theorem MonoidHom.range_one

added theorem MonoidHom.range_top_iff_surjective

added theorem MonoidHom.range_top_of_surjective

added theorem MonoidHom.restrict_range

added def MonoidHom.subgroupComap

added def MonoidHom.subgroupMap

added theorem MonoidHom.subgroupMap_surjective

added theorem MonoidHom.subgroupOf_range_eq_of_le

added theorem MonoidHom.subtype_comp_rangeRestrict

added theorem MulEquiv.coe_subgroupMap_apply

added def MulEquiv.subgroupCongr

added def MulEquiv.subgroupMap

added theorem MulEquiv.subgroupMap_symm_apply

added def NormalizerCondition

added structure Subgroup.Characteristic

added structure Subgroup.IsCommutative

added theorem Subgroup.Normal.comap

added theorem Subgroup.Normal.map

added theorem Subgroup.Normal.mem_comm

added theorem Subgroup.Normal.mem_comm_iff

added theorem Subgroup.Normal.subgroupOf

added structure Subgroup.Normal

added theorem Subgroup.NormalizerCondition.normal_of_coatom

added def Subgroup.Simps.coe

added theorem Subgroup.SubgroupNormal.mem_comm

added theorem Subgroup.apply_coe_mem_map

added theorem Subgroup.bot_or_exists_ne_one

added theorem Subgroup.bot_or_nontrivial

added theorem Subgroup.bot_prod_bot

added theorem Subgroup.bot_subgroupOf

added theorem Subgroup.bot_toSubmonoid

added def Subgroup.center

added theorem Subgroup.center_le_normalizer

added theorem Subgroup.center_toSubmonoid

added def Subgroup.centralizer

added theorem Subgroup.centralizer_le

added theorem Subgroup.centralizer_top

added theorem Subgroup.characteristic_iff_comap_eq

added theorem Subgroup.characteristic_iff_comap_le

added theorem Subgroup.characteristic_iff_le_comap

added theorem Subgroup.characteristic_iff_le_map

added theorem Subgroup.characteristic_iff_map_eq

added theorem Subgroup.characteristic_iff_map_le

added def Subgroup.closure

added def Subgroup.closureCommGroupOfComm

added theorem Subgroup.closure_closure_coe_preimage

added theorem Subgroup.closure_empty

added theorem Subgroup.closure_eq

added theorem Subgroup.closure_eq_bot_iff

added theorem Subgroup.closure_eq_of_le

added theorem Subgroup.closure_eq_top_of_mclosure_eq_top

added theorem Subgroup.closure_induction'

added theorem Subgroup.closure_induction

added theorem Subgroup.closure_induction₂

added theorem Subgroup.closure_le

added theorem Subgroup.closure_le_normalClosure

added theorem Subgroup.closure_mono

added theorem Subgroup.closure_preimage_eq_top

added theorem Subgroup.closure_singleton_one

added theorem Subgroup.closure_union

added theorem Subgroup.closure_unionᵢ

added theorem Subgroup.closure_univ

added theorem Subgroup.codisjoint_subgroupOf_sup

added theorem Subgroup.coeSubtype

added theorem Subgroup.coe_bot

added theorem Subgroup.coe_center

added theorem Subgroup.coe_comap

added theorem Subgroup.coe_copy

added theorem Subgroup.coe_div

added theorem Subgroup.coe_eq_singleton

added theorem Subgroup.coe_eq_univ

added theorem Subgroup.coe_equivMapOfInjective_apply

added theorem Subgroup.coe_inclusion

added theorem Subgroup.coe_inf

added theorem Subgroup.coe_infᵢ

added theorem Subgroup.coe_infₛ

added theorem Subgroup.coe_inv

added theorem Subgroup.coe_map

added theorem Subgroup.coe_mk

added theorem Subgroup.coe_mul

added theorem Subgroup.coe_one

added theorem Subgroup.coe_pi

added theorem Subgroup.coe_pow

added theorem Subgroup.coe_prod

added theorem Subgroup.coe_set_mk

added theorem Subgroup.coe_subgroupOf

added theorem Subgroup.coe_supᵢ_of_directed

added theorem Subgroup.coe_toSubmonoid

added theorem Subgroup.coe_top

added theorem Subgroup.coe_zpow

added def Subgroup.comap

added theorem Subgroup.comap_comap

added theorem Subgroup.comap_equiv_eq_map_symm

added theorem Subgroup.comap_id

added theorem Subgroup.comap_inclusion_subgroupOf

added theorem Subgroup.comap_inf

added theorem Subgroup.comap_infᵢ

added theorem Subgroup.comap_injective

added theorem Subgroup.comap_injective_isCommutative

added theorem Subgroup.comap_le_comap_of_le_range

added theorem Subgroup.comap_le_comap_of_surjective

added theorem Subgroup.comap_lt_comap_of_surjective

added theorem Subgroup.comap_map_eq

added theorem Subgroup.comap_map_eq_self

added theorem Subgroup.comap_map_eq_self_of_injective

added theorem Subgroup.comap_mono

added theorem Subgroup.comap_normalizer_eq_of_injective_of_le_range

added theorem Subgroup.comap_normalizer_eq_of_surjective

added theorem Subgroup.comap_subtype

added theorem Subgroup.comap_sup_comap_le

added theorem Subgroup.comap_sup_eq

added theorem Subgroup.comap_sup_eq_of_le_range

added theorem Subgroup.comap_top

added theorem Subgroup.commute_of_normal_of_disjoint

added theorem Subgroup.conjugatesOfSet_subset_normalClosure

added theorem Subgroup.copy_eq

added theorem Subgroup.disjoint_def'

added theorem Subgroup.disjoint_def

added theorem Subgroup.disjoint_iff_mul_eq_one

added theorem Subgroup.eq_bot_iff_forall

added theorem Subgroup.eq_bot_of_subsingleton

added theorem Subgroup.eq_top_iff'

added theorem Subgroup.equivMapOfInjective_coe_mulEquiv

added theorem Subgroup.ext

added theorem Subgroup.gc_map_comap

added def Subgroup.inclusion

added theorem Subgroup.inclusion_injective

added theorem Subgroup.inclusion_range

added theorem Subgroup.inf_subgroupOf_inf_normal_of_left

added theorem Subgroup.inf_subgroupOf_inf_normal_of_right

added theorem Subgroup.inf_subgroupOf_left

added theorem Subgroup.inf_subgroupOf_right

added theorem Subgroup.ker_inclusion

added theorem Subgroup.ker_le_comap

added theorem Subgroup.ker_subtype

added theorem Subgroup.le_centralizer

added theorem Subgroup.le_centralizer_iff

added theorem Subgroup.le_centralizer_iff_isCommutative

added theorem Subgroup.le_closure_toSubmonoid

added theorem Subgroup.le_comap_map

added theorem Subgroup.le_normalClosure

added theorem Subgroup.le_normalizer

added theorem Subgroup.le_normalizer_comap

added theorem Subgroup.le_normalizer_map

added theorem Subgroup.le_normalizer_of_normal

added theorem Subgroup.le_pi_iff

added theorem Subgroup.le_prod_iff

added def Subgroup.map

added theorem Subgroup.map_bot

added theorem Subgroup.map_comap_eq

added theorem Subgroup.map_comap_eq_self

added theorem Subgroup.map_comap_eq_self_of_surjective

added theorem Subgroup.map_comap_le

added theorem Subgroup.map_eq_bot_iff

added theorem Subgroup.map_eq_bot_iff_of_injective

added theorem Subgroup.map_eq_comap_of_inverse

added theorem Subgroup.map_eq_map_iff

added theorem Subgroup.map_eq_range_iff

added theorem Subgroup.map_equiv_eq_comap_symm

added theorem Subgroup.map_equiv_normalizer_eq

added theorem Subgroup.map_id

added theorem Subgroup.map_inf_eq

added theorem Subgroup.map_inf_le

added theorem Subgroup.map_injective

added theorem Subgroup.map_injective_of_ker_le

added theorem Subgroup.map_le_iff_le_comap

added theorem Subgroup.map_le_map_iff'

added theorem Subgroup.map_le_map_iff

added theorem Subgroup.map_le_map_iff_of_injective

added theorem Subgroup.map_le_range

added theorem Subgroup.map_map

added theorem Subgroup.map_mono

added theorem Subgroup.map_normalizer_eq_of_bijective

added theorem Subgroup.map_one_eq_bot

added theorem Subgroup.map_subtype_le

added theorem Subgroup.map_subtype_le_map_subtype

added theorem Subgroup.map_sup

added theorem Subgroup.map_supᵢ

added theorem Subgroup.map_symm_eq_iff_map_eq

added theorem Subgroup.map_top_of_surjective

added theorem Subgroup.mem_bot

added theorem Subgroup.mem_carrier

added theorem Subgroup.mem_center_iff

added theorem Subgroup.mem_centralizer_iff

added theorem Subgroup.mem_centralizer_iff_commutator_eq_one

added theorem Subgroup.mem_closure

added theorem Subgroup.mem_closure_pair

added theorem Subgroup.mem_closure_singleton

added theorem Subgroup.mem_comap

added theorem Subgroup.mem_inf

added theorem Subgroup.mem_infᵢ

added theorem Subgroup.mem_infₛ

added theorem Subgroup.mem_map

added theorem Subgroup.mem_map_equiv

added theorem Subgroup.mem_map_iff_mem

added theorem Subgroup.mem_map_of_mem

added theorem Subgroup.mem_mk

added theorem Subgroup.mem_normalizer_iff''

added theorem Subgroup.mem_normalizer_iff'

added theorem Subgroup.mem_normalizer_iff

added theorem Subgroup.mem_pi

added theorem Subgroup.mem_prod

added theorem Subgroup.mem_subgroupOf

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_supᵢ_of_directed

added theorem Subgroup.mem_supᵢ_of_mem

added theorem Subgroup.mem_supₛ_of_directedOn

added theorem Subgroup.mem_supₛ_of_mem

added theorem Subgroup.mem_toSubmonoid

added theorem Subgroup.mem_top

added theorem Subgroup.mk_eq_one_iff

added theorem Subgroup.mk_le_mk

added theorem Subgroup.mulSingle_mem_pi

added theorem Subgroup.mul_injective_of_disjoint

added theorem Subgroup.mul_mem_sup

added theorem Subgroup.nontrivial_iff

added theorem Subgroup.nontrivial_iff_exists_ne_one

added def Subgroup.normalClosure

added theorem Subgroup.normalClosure_closure_eq_normalClosure

added theorem Subgroup.normalClosure_eq_infᵢ

added theorem Subgroup.normalClosure_eq_self

added theorem Subgroup.normalClosure_idempotent

added theorem Subgroup.normalClosure_le_normal

added theorem Subgroup.normalClosure_mono

added theorem Subgroup.normalClosure_subset_iff

added def Subgroup.normalCore

added theorem Subgroup.normalCore_eq_self

added theorem Subgroup.normalCore_eq_supᵢ

added theorem Subgroup.normalCore_idempotent

added theorem Subgroup.normalCore_le

added theorem Subgroup.normalCore_mono

added theorem Subgroup.normal_le_normalCore

added theorem Subgroup.normal_subgroupOf_iff

added def Subgroup.normalizer

added theorem Subgroup.normalizer_eq_top

added theorem Subgroup.not_mem_of_not_mem_closure

added def Subgroup.ofDiv

added def Subgroup.pi

added theorem Subgroup.pi_bot

added theorem Subgroup.pi_empty

added theorem Subgroup.pi_eq_bot_iff

added theorem Subgroup.pi_top

added def Subgroup.prod

added def Subgroup.prodEquiv

added theorem Subgroup.prod_eq_bot_iff

added theorem Subgroup.prod_le_iff

added theorem Subgroup.prod_mono

added theorem Subgroup.prod_mono_left

added theorem Subgroup.prod_mono_right

added theorem Subgroup.prod_top

added def Subgroup.setNormalizer

added def Subgroup.subgroupOf

added def Subgroup.subgroupOfEquivOfLe

added theorem Subgroup.subgroupOf_bot_eq_bot

added theorem Subgroup.subgroupOf_bot_eq_top

added theorem Subgroup.subgroupOf_eq_bot

added theorem Subgroup.subgroupOf_eq_top

added theorem Subgroup.subgroupOf_inj

added theorem Subgroup.subgroupOf_map_subtype

added theorem Subgroup.subgroupOf_normalizer_eq

added theorem Subgroup.subgroupOf_self

added theorem Subgroup.subgroupOf_sup

added theorem Subgroup.subset_closure

added theorem Subgroup.subset_normalClosure

added theorem Subgroup.subsingleton_iff

added def Subgroup.subtype

added theorem Subgroup.subtype_comp_inclusion

added theorem Subgroup.subtype_injective

added theorem Subgroup.subtype_range

added theorem Subgroup.sup_subgroupOf_eq

added theorem Subgroup.supᵢ_comap_le

added theorem Subgroup.supᵢ_eq_closure

added def Subgroup.toAddSubgroup

added theorem Subgroup.toSubmonoid_eq

added theorem Subgroup.toSubmonoid_injective

added theorem Subgroup.toSubmonoid_le

added theorem Subgroup.toSubmonoid_mono

added theorem Subgroup.toSubmonoid_strictMono

added def Subgroup.topEquiv

added theorem Subgroup.top_prod

added theorem Subgroup.top_prod_top

added theorem Subgroup.top_subgroupOf

added theorem Subgroup.top_toSubmonoid

added structure Subgroup

added theorem SubgroupClass.coeSubtype

added theorem SubgroupClass.coe_div

added theorem SubgroupClass.coe_inclusion

added theorem SubgroupClass.coe_inv

added theorem SubgroupClass.coe_pow

added theorem SubgroupClass.coe_zpow

added def SubgroupClass.inclusion

added theorem SubgroupClass.inclusion_inclusion

added theorem SubgroupClass.inclusion_mk

added theorem SubgroupClass.inclusion_right

added theorem SubgroupClass.inclusion_self

added def SubgroupClass.subtype

added theorem SubgroupClass.subtype_comp_inclusion

added def Submonoid.pi

added theorem div_mem

added theorem div_mem_comm_iff

added theorem exists_inv_mem_iff_exists_mem

added theorem inv_mem_iff

added theorem mul_mem_cancel_left

added theorem mul_mem_cancel_right

added theorem normalizerCondition_iff_only_full_group_self_normalizing

added theorem zpow_mem