English
If P is a Sylow p-subgroup, then P is not the trivial subgroup when |G|≥1; in particular, P ≠ ⊥.
Русский
Если P — Sylow p-подгруппа, то она не тривиальная, то есть P ≠ ⊥.
LaTeX
$$(P : Subgroup G) ≠ ⊥$$
Lean4
theorem ne_bot_of_dvd_card [Finite G] {p : ℕ} [hp : Fact p.Prime] (P : Sylow p G) (hdvd : p ∣ Nat.card G) :
(P : Subgroup G) ≠ ⊥ := by
refine fun h => hp.out.not_dvd_one ?_
have key : p ∣ Nat.card P := P.dvd_card_of_dvd_card hdvd
rwa [h, card_bot] at key