card_eq_card_quotient_normalizer — Mathlib

English

There is a bijection between Sylow_p(G) and G / N_G(P), hence their cardinalities are equal: |Sylow_p(G)| = |G / N_G(P)|.

Русский

Существует биекция между Sylow_p(G) и G / N_G(P); следовательно, их мощности равны: |Sylow_p(G)| = |G / N_G(P)|.

LaTeX

$$$|\\mathrm{Sylow}_p(G)| = |G / N_G(P)|.$$$

Lean4

theorem card_eq_card_quotient_normalizer [Fact p.Prime] [Finite (Sylow p G)] (P : Sylow p G) :
    Nat.card (Sylow p G) = Nat.card (G ⧸ P.normalizer) :=
  Nat.card_congr P.equivQuotientNormalizer

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