Theorem nodup_permsOfList

Modification history

2023-12-25 13:26

Mathlib/Data/Fintype/Perm.lean

chore(*): use `∃ x ∈ s, _` instead of `∃ (x) (_ : x ∈ s), _` (#9215) …

Modified nodup_permsOfList View on Github →

2023-02-05 17:34

Mathlib/Data/Fintype/Perm.lean

feat: Port Data.Fintype.Perm (#1691) …

Added nodup_permsOfList View on Github →