Commit 2023-07-11 12:40 bd365b1a

feat(group_theory/sylow): add inverse to card_eq_multiplicity (#18300) The lemma card_eq_multiplicity states that a Sylow group of a finite group has cardinality p^n, where n is the multiplicity of p in the group order. This PR adds an inverse definition card_eq_multiplicity_to_sylow, promoting a subgroup of the right cardinality to a Sylow group, and a simplification lemma coe_card_eq_multiplicity_to_sylow for the coercion of the resulting Sylow group back to a subgroup.