Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2020-12-08 10:43 51f5ca3e

View on Github →

chore(group_theory/perm): Add alternate formulation of (sum|sigma)_congr lemmas (#5260) These lemmas existed already for equiv, but not for perm or for perm via group structures.

Estimated changes

Modified src/data/equiv/basic.lean

added def equiv.perm.sigma_congr_right

added theorem equiv.perm.sigma_congr_right_refl

added theorem equiv.perm.sigma_congr_right_symm

added theorem equiv.perm.sigma_congr_right_trans

added def equiv.perm.sum_congr

added theorem equiv.perm.sum_congr_apply

added theorem equiv.perm.sum_congr_refl

added theorem equiv.perm.sum_congr_symm

added theorem equiv.perm.sum_congr_trans

modified theorem equiv.sum_congr_symm

Modified src/group_theory/perm/basic.lean

added theorem equiv.perm.sigma_congr_right_inv

added theorem equiv.perm.sigma_congr_right_mul

added theorem equiv.perm.sigma_congr_right_one

added theorem equiv.perm.sum_congr_inv

added theorem equiv.perm.sum_congr_mul

added theorem equiv.perm.sum_congr_one