coprime_commutator_index — Mathlib

English

If a finite Z-group G has a coprime Sylow p-subgroup structure, then card of the commutator and its index are coprime.

Русский

У конечной Z-группы G карта коммутатора и его индекс взаимно просты.

LaTeX

$$$(\\operatorname{card}(\\operatorname{commutator} G)).Coprime(\\operatorname{commutator} G).index$$$

Lean4

/-- If `G` is a finite Z-group, then `commutator G` is a Hall subgroup of `G`. -/
theorem coprime_commutator_index [Finite G] [IsZGroup G] : (Nat.card (commutator G)).Coprime (commutator G).index :=
  by
  suffices h : ∀ p, p.Prime → (¬p ∣ Nat.card (commutator G) ∨ ¬p ∣ (commutator G).index)
    by
    contrapose! h
    exact Nat.Prime.not_coprime_iff_dvd.mp h
  intro p hp
  have := Fact.mk hp
  exact Sylow.not_dvd_card_commutator_or_not_dvd_index_commutator default

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