coe_ofCard — Mathlib

English

If a subgroup H has cardinality equal to p^{|G|.factorization p}, then Sylow.ofCard H card_eq is precisely the Sylow p-subgroup whose underlying subgroup is H.

Русский

Если подгруппа H имеет кардинальность p^{|G|.factorization p}, то Sylow.ofCard H card_eq есть именно Силова p-подгруппа, основанная на H.

LaTeX

$$$ (Sylow.ofCard H card\_eq).toSubgroup = H $$$

Lean4

@[simp, norm_cast]
theorem coe_ofCard [Finite G] {p : ℕ} [Fact p.Prime] (H : Subgroup G)
    (card_eq : Nat.card H = p ^ (Nat.card G).factorization p) : ofCard H card_eq = H :=
  rfl

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