not_dvd_card_sylow — Mathlib

English

For prime p and finite Sylow p-subgroups, p does not divide the cardinality of Sylow_p(G).

Русский

Для простого p и конечной Sylow_p(G) число |Sylow_p(G)| не делится на p.

LaTeX

$$$\\neg p \\mid |\\mathrm{Sylow}_p(G)|.$$$

Lean4

theorem not_dvd_card_sylow [hp : Fact p.Prime] [Finite (Sylow p G)] : ¬p ∣ Nat.card (Sylow p G) := fun h =>
  hp.1.ne_one
    (Nat.dvd_one.mp
      ((Nat.modEq_iff_dvd' zero_le_one).mp ((Nat.modEq_zero_iff_dvd.mpr h).symm.trans (card_sylow_modEq_one p G))))

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