doc(group_theory/sylow): update docstring to include card_eq_multipli…

…city as a main result (#14354)

Sylow subgroups have been redefined to be maximal p-subgroups, instead of subgroups of cardinality `p^n` where `n` is the multiplicity of `p` in the cardinality of G. Sylow's first theorem basically proves that these two are equivalent. With the new definition the hard part of Sylow's first theorem is really proving the lemma `sylow.card_eq_multiplicity` and not proving the existence of a Sylow subgroup so I included it as a main result.

src/group_theory/sylow.lean

@@ -32,6 +32,8 @@ The Sylow theorems are the following results for every finite group `G` and ever
   there exists a subgroup of `G` of order `pⁿ`.
 * `is_p_group.exists_le_sylow`: A generalization of Sylow's first theorem:
   Every `p`-subgroup is contained in a Sylow `p`-subgroup.
+* `sylow.card_eq_multiplicity`: The cardinality of a Sylow group is `p ^ n`
+ where `n` is the multiplicity of `p` in the group order.
 * `sylow_conjugate`: A generalization of Sylow's second theorem:
   If the number of Sylow `p`-subgroups is finite, then all Sylow `p`-subgroups are conjugate.
 * `card_sylow_modeq_one`: A generalization of Sylow's third theorem: