Theorem List.formPerm_eq_self_of_notMem

Modification history

2025-10-07 10:51

Mathlib/GroupTheory/Perm/List.lean

chore(GroupTheory/Perm): deprecate `mem_of_formPerm_ne_self` and `formPerm_eq_self_of_notMem` (#28441)

Deleted List.formPerm_eq_self_of_notMem View on Github →

2025-05-25 12:30

Mathlib/GroupTheory/Perm/List.lean

chore(*): not_mem/nmem -> notMem (#25159)

Added List.formPerm_eq_self_of_notMem View on Github →