feat(group_theory/transfer): `¬ p ∣ card transfer_sylow.ker` (#17502)
feat(group_theory/transfer): `¬ p ∣ card transfer_sylow.ker` (#17502)

This PR adds a lemma stating that the cardinality of the kernel of `transfer_sylow` is indivisible by `p`.





leanprover-community/mathlib,leanprover-community/mathlib