Theorems · Theorem · group theory

Subgroup.normal_of_index_eq_minFac_card

∀ {G : Type u_1} [inst : Group G] {H : Subgroup G}, H.index = (Nat.card G).minFac → H.Normal

A subgroup of a finite group whose index is the smallest prime factor is normal. Note : if G is infinite, then Nat.card G = 0 and (Nat.card G).minFac = 2

Defined in

Mathlib.GroupTheory.IndexNormal

Cited by

0 results in Mathlib

Foundations

Depth 100 from the axioms · uses propext, Classical.choice, Quot.sound

Assumes

Group