ne_bot_of_dvd_card — Mathlib

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

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