mathlib3

56489b55 - refactor(group_theory/transfer): Golf proof of `ker_transfer_sylow_disjoint` (#17661)

refactor(group_theory/transfer): Golf proof of `ker_transfer_sylow_disjoint` (#17661) Currently `transfer.lean` contains three versions of `ker_transfer_sylow_disjoint`, in increasing generality, proved in succession. But `not_dvd_card_ker_transfer_sylow` can be used to give a quick proof of the most general version, rendering the less general versions obsolete.