frattini_nongenerating — Mathlib

English

If a subgroup K together with the Frattini subgroup generates the whole group, then K is already the whole group.

Русский

Если подгруппа K и Frattini(G) порождают всю группу, то K уже равна всей группе.

LaTeX

$$$K \\lor \\operatorname{frattini}(G) = G \\Rightarrow K = G$$$

Lean4

/-- The Frattini subgroup consists of "non-generating" elements in the following sense:

If a subgroup together with the Frattini subgroup generates the whole group,
then the subgroup is already the whole group.
-/
theorem frattini_nongenerating [IsCoatomic (Subgroup G)] {K : Subgroup G} (h : K ⊔ frattini G = ⊤) : K = ⊤ :=
  Order.radical_nongenerating h

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