mathlib

e1783b0f - doc(group_theory/sylow): update docstring to include card_eq_multiplicity as a main result (#14354)

doc(group_theory/sylow): update docstring to include card_eq_multiplicity 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.