doc(group_theory/sylow): Expand Frattini's argument docstring (#10174)

Expands the docstring for Frattini's argument.
leanprover-community · Nov 5, 2021 · 6f9ec12 · 6f9ec12
1 parent 8490f2a
commit 6f9ec12
Showing 1 changed file with 2 additions and 1 deletion.
diff --git a/src/group_theory/sylow.lean b/src/group_theory/sylow.lean
@@ -217,7 +217,8 @@ lemma card_sylow_dvd_index [fact p.prime] [fintype (sylow p G)] (P : sylow p G)
   card (sylow p G) ∣ P.1.index :=
 ((congr_arg _ (card_sylow_eq_index_normalizer P)).mp dvd_rfl).trans (index_dvd_of_le le_normalizer)
 
-/-- Frattini's Argument -/
+/-- Frattini's Argument: If `N` is a normal subgroup of `G`, and if `P` is a Sylow `p`-subgroup
+  of `N`, then `N_G(P) ⊔ N = G`. -/
 lemma sylow.normalizer_sup_eq_top {p : ℕ} [fact p.prime] {N : subgroup G} [N.normal]
   [fintype (sylow p N)] (P : sylow p N) : ((↑P : subgroup N).map N.subtype).normalizer ⊔ N = ⊤ :=
 begin