mathlib

bd365b1a - feat(group_theory/sylow): add inverse to card_eq_multiplicity (#18300)

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.