Commit 2023-03-26 23:21 027df748

View on Github →

chore: sync Data.List.Perm (#3076)

Estimated changes

Modified Mathlib/Data/List/Perm.lean

deleted theorem List.Perm.eq_singleton

deleted theorem List.Perm.singleton_eq