Commit 2023-06-05 17:06 17f92ef5

View on Github →

feat: port GroupTheory.Transfer (#4482)

Estimated changes

Modified Mathlib.lean

Created Mathlib/GroupTheory/Transfer.lean

added theorem MonoidHom.ker_transferSylow_disjoint

added theorem MonoidHom.ker_transferSylow_isComplement'

added theorem MonoidHom.not_dvd_card_ker_transferSylow

added theorem MonoidHom.transferCenterPow_apply

added theorem MonoidHom.transferSylow_eq_pow

added theorem MonoidHom.transferSylow_restrict_eq_pow

added theorem MonoidHom.transfer_center_eq_pow

added theorem MonoidHom.transfer_def

added theorem MonoidHom.transfer_eq_pow

added theorem MonoidHom.transfer_eq_pow_aux

added theorem MonoidHom.transfer_eq_prod_quotient_orbitRel_zpowers_quot

added theorem MonoidHom.transfer_sylow_eq_pow_aux

added theorem Subgroup.leftTransversals.diff_inv

added theorem Subgroup.leftTransversals.diff_mul_diff

added theorem Subgroup.leftTransversals.diff_self

added theorem Subgroup.leftTransversals.smul_diff_smul