mathlib3

0013cf77 - 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`.