Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2020-12-10 13:58 3f42fb48

View on Github →

feat(group_theory/perm/sign): Add sign_sum_congr (#5266)

Estimated changes

Modified src/data/equiv/basic.lean

added theorem equiv.perm.sum_congr_refl_swap

added theorem equiv.perm.sum_congr_swap_refl

Modified src/group_theory/perm/basic.lean

added theorem equiv.perm.sum_congr_one_swap

added theorem equiv.perm.sum_congr_swap_one

Modified src/group_theory/perm/sign.lean

added theorem equiv.perm.sign_sum_congr