# 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.

Mathlib v3 is deprecated. Go to Mathlib v4

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.