mathlib

47c60812 - chore(group_theory/perm/sign): remove classical for sign congr simp lemmas (#5622)

chore(group_theory/perm/sign): remove classical for sign congr simp lemmas (#5622) Previously, some lemmas about how `perm.sign` simplifies across various congrs of permutations assumed `classical`, which prevented them from being applied by the simplifier. This makes the `decidable_eq` assumptions explicit.