Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2022-04-21 23:36 d444a279

View on Github →

feat(group_theory/transfer): Define the transfer homomorphism (#13446) This PR adds a definition of the transfer homomorphism.

Estimated changes

Created src/group_theory/transfer.lean

added theorem monoid_hom.transfer_def

added theorem subgroup.left_transversals.diff_inv

added theorem subgroup.left_transversals.diff_mul_diff

added theorem subgroup.left_transversals.diff_self

added theorem subgroup.left_transversals.smul_diff_smul