English
If p is prime and Sylow_p(G) is finite, then |Sylow_p(G)| ≡ 1 (mod p).
Русский
Если p — простое и Sylow_p(G) конечно, то |Sylow_p(G)| ≡ 1 (mod p).
LaTeX
$$$\\lvert \\mathrm{Sylow}_p(G)\\rvert \\equiv 1 \\pmod p.$$$
Lean4
/-- A generalization of **Sylow's third theorem**.
If the number of Sylow `p`-subgroups is finite, then it is congruent to `1` modulo `p`. -/
theorem card_sylow_modEq_one [Fact p.Prime] [Finite (Sylow p G)] : Nat.card (Sylow p G) ≡ 1 [MOD p] :=
by
refine Sylow.nonempty.elim fun P : Sylow p G => ?_
have : fixedPoints P.1 (Sylow p G) = { P } :=
Set.ext fun Q : Sylow p G =>
calc
Q ∈ fixedPoints P (Sylow p G) ↔ P.1 ≤ Q := P.2.sylow_mem_fixedPoints_iff
_ ↔ Q.1 = P.1 := ⟨P.3 Q.2, ge_of_eq⟩
_ ↔ Q ∈ { P } := Sylow.ext_iff.symm.trans Set.mem_singleton_iff.symm
have : Nat.card (fixedPoints P.1 (Sylow p G)) = 1 := by simp [this]
exact (P.2.card_modEq_card_fixedPoints (Sylow p G)).trans (by rw [this])
