Theorem Equiv.Perm.signAux3_symm_trans_trans

Modification history

2024-02-27 06:49

Mathlib/GroupTheory/Perm/Sign.lean

chore(GroupTheory/Perm): drop `DecidableEq`, `Fintype` -> `Finite` (#10917)

Modified Equiv.Perm.signAux3_symm_trans_trans View on Github →

2023-02-27 13:06

Mathlib/GroupTheory/Perm/Sign.lean

feat: port GroupTheory.Perm.Sign (#2458)

Added Equiv.Perm.signAux3_symm_trans_trans View on Github →