Commit 2021-01-07 10:05 47c60812
View on Github →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.