Commit 2023-05-29 09:35 37fa523f

View on Github →

feat: port GroupTheory.Sylow (#4387)

Estimated changes

Modified Mathlib.lean

Created Mathlib/GroupTheory/Sylow.lean

added theorem IsPGroup.exists_le_sylow

added theorem IsPGroup.inf_normalizer_sylow

added theorem IsPGroup.sylow_mem_fixedPoints_iff

added theorem QuotientGroup.card_preimage_mk

added theorem Subgroup.sylow_mem_fixedPoints_iff

added theorem Sylow.card_coprime_index

added theorem Sylow.card_eq_multiplicity

added theorem Sylow.card_normalizer_modEq_card

added theorem Sylow.card_quotient_normalizer_modEq_card_quotient

added theorem Sylow.characteristic_of_normal

added theorem Sylow.coe_comapOfInjective

added theorem Sylow.coe_comapOfKerIsPGroup

added theorem Sylow.coe_smul

added theorem Sylow.coe_subgroup_smul

added theorem Sylow.coe_subtype

added def Sylow.comapOfInjective

added def Sylow.comapOfKerIsPGroup

added theorem Sylow.conj_eq_normalizer_conj_of_mem

added theorem Sylow.conj_eq_normalizer_conj_of_mem_centralizer

added theorem Sylow.dvd_card_of_dvd_card

added theorem Sylow.exists_comap_eq_of_injective

added theorem Sylow.exists_comap_eq_of_ker_isPGroup

added theorem Sylow.exists_comap_subtype_eq

added theorem Sylow.exists_subgroup_card_pow_prime

added theorem Sylow.exists_subgroup_card_pow_prime_le

added theorem Sylow.exists_subgroup_card_pow_succ

added theorem Sylow.ext

added theorem Sylow.ext_iff

added def Sylow.fixedPointsMulLeftCosetsEquivQuotient

added theorem Sylow.mem_fixedPoints_mul_left_cosets_iff_mem_normalizer

added theorem Sylow.ne_bot_of_dvd_card

added theorem Sylow.normal_of_all_max_subgroups_normal

added theorem Sylow.normal_of_normalizerCondition

added theorem Sylow.normal_of_normalizer_normal

added theorem Sylow.normalizer_normalizer

added theorem Sylow.normalizer_sup_eq_top'

added theorem Sylow.normalizer_sup_eq_top

added theorem Sylow.orbit_eq_top

added theorem Sylow.pointwise_smul_def

added theorem Sylow.pow_dvd_card_of_pow_dvd_card

added theorem Sylow.prime_dvd_card_quotient_normalizer

added theorem Sylow.prime_pow_dvd_card_normalizer

added theorem Sylow.smul_def

added theorem Sylow.smul_eq_iff_mem_normalizer

added theorem Sylow.smul_eq_of_normal

added theorem Sylow.smul_le

added theorem Sylow.smul_subtype

added theorem Sylow.stabilizer_eq_normalizer

added theorem Sylow.subsingleton_of_normal

added theorem Sylow.subtype_injective

added structure Sylow

added theorem card_sylow_dvd_index

added theorem card_sylow_eq_card_quotient_normalizer

added theorem card_sylow_eq_index_normalizer

added theorem card_sylow_modEq_one

added theorem not_dvd_card_sylow

added theorem not_dvd_index_sylow'

added theorem not_dvd_index_sylow