Commit 2022-11-20 15:51 0013cf77

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.