Commit 2024-11-08 14:58 7f2ea3e1

View on Github →

refactor(GroupTheory/Sylow): use namespacing and dot-notation (#18750) This PR cleans up Sylow.lean by using namespacing and dot-notation.

Estimated changes

Modified Mathlib/GroupTheory/Sylow.lean

added theorem Sylow.card_dvd_index

added theorem Sylow.card_eq_card_quotient_normalizer

added theorem Sylow.card_eq_index_normalizer

modified theorem Sylow.coe_comapOfInjective

modified theorem Sylow.coe_comapOfKerIsPGroup

modified theorem Sylow.coe_smul

modified theorem Sylow.coe_subgroup_smul

modified theorem Sylow.coe_subtype

modified def Sylow.comapOfInjective

modified def Sylow.comapOfKerIsPGroup

modified theorem Sylow.conj_eq_normalizer_conj_of_mem

modified theorem Sylow.conj_eq_normalizer_conj_of_mem_centralizer

modified theorem Sylow.exists_comap_eq_of_injective

modified theorem Sylow.exists_comap_eq_of_ker_isPGroup

modified theorem Sylow.exists_comap_subtype_eq

modified theorem Sylow.finite_of_injective

modified theorem Sylow.finite_of_ker_is_pGroup

modified theorem Sylow.normalizer_sup_eq_top'

modified theorem Sylow.normalizer_sup_eq_top

modified theorem Sylow.not_dvd_index'

modified theorem Sylow.not_dvd_index

modified theorem Sylow.orbit_eq_top

modified theorem Sylow.pointwise_smul_def

modified theorem Sylow.smul_def

modified theorem Sylow.smul_eq_iff_mem_normalizer

modified theorem Sylow.smul_eq_of_normal

modified theorem Sylow.smul_le

modified theorem Sylow.smul_subtype

modified theorem Sylow.stabilizer_eq_normalizer

modified theorem Sylow.subtype_injective

deleted theorem card_sylow_dvd_index

deleted theorem card_sylow_eq_card_quotient_normalizer

deleted theorem card_sylow_eq_index_normalizer