Mathlib v3 is deprecated. Go to Mathlib v4

Theorem monoid_hom.not_dvd_card_ker_transfer_sylow

Modification history

2022-11-20 15:51
src/group_theory/transfer.lean
feat(group_theory/transfer): `¬ p ∣ card transfer_sylow.ker` (#17502) …
Added monoid_hom.not_dvd_card_ker_transfer_sylowView on Github →