not_dvd_card_commutator_or_not_dvd_index_commutator

English

If G has a cyclic Sylow p-subgroup, then p cannot divide both |commutator G| and the index [G:commutator G].

Русский

Если у G циклическая сигма-p-подгруппа, то p не делит одновременно |коммутатора(G)| и индекс [G : коммутатор(G)].

LaTeX

$$$\\neg p \\mid |\\mathrm{commutator}(G)| \\lor \\neg p \\mid (\\mathrm{commutator}(G)).index$$$

Lean4

/-- If `G` has a cyclic Sylow `p`-subgroup, then the cardinality and index of the commutator
  subgroup of `G` cannot both be divisible by `p`. -/
theorem not_dvd_card_commutator_or_not_dvd_index_commutator :
    ¬p ∣ Nat.card (commutator G) ∨ ¬p ∣ (commutator G).index :=
  by
  refine (normalizer_le_centralizer_or_le_commutator P).imp ?_ ?_ <;> refine fun hP h ↦ P.not_dvd_index (h.trans ?_)
  · rw [(MonoidHom.ker_transferSylow_isComplement' P hP).index_eq_card]
    exact Subgroup.card_dvd_of_le (Abelianization.commutator_subset_ker _)
  · exact Subgroup.index_dvd_of_le hP

Похожие утверждения