mathlib
51f5ca3e - chore(group_theory/perm): Add alternate formulation of (sum|sigma)_congr lemmas (#5260)

Commit

5 years ago

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.

Author

eric-wieser

Parents

ac6fc38e

mathlib 51f5ca3e - chore(group_theory/perm): Add alternate formulation of (sum|sigma)_congr lemmas (#5260)

mathlib
51f5ca3e - chore(group_theory/perm): Add alternate formulation of (sum|sigma)_congr lemmas (#5260)