Commit 2022-11-20 15:51 0013cf77

View on Github →

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.

Estimated changes