Skip to content

Commit 483fd28

Browse files
authored
chore: fix name of List.singleton_subperm_iff (#429)
1 parent 604b407 commit 483fd28

File tree

1 file changed

+1
-1
lines changed

1 file changed

+1
-1
lines changed

Std/Data/List/Perm.lean

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -252,7 +252,7 @@ theorem Subperm.filter (p : α → Bool) ⦃l l' : List α⦄ (h : l <+~ l') :
252252
let ⟨xs, hp, h⟩ := h
253253
exact ⟨_, hp.filter p, h.filter p⟩
254254

255-
@[simp] theorem subperm_singleton_iff {α} {l : List α} {a : α} : [a] <+~ l ↔ a ∈ l := by
255+
@[simp] theorem singleton_subperm_iff {α} {l : List α} {a : α} : [a] <+~ l ↔ a ∈ l := by
256256
refine ⟨fun ⟨s, hla, h⟩ => ?_, fun h => ⟨[a], .rfl, singleton_sublist.mpr h⟩⟩
257257
rwa [perm_singleton.mp hla, singleton_sublist] at h
258258

0 commit comments

Comments
 (0)