remove duplicate

leanprover-community · Sep 11, 2024 · 707ae20 · 707ae20
1 parent ccb095d
commit 707ae20
Showing 1 changed file with 0 additions and 2 deletions.
diff --git a/Batteries/Data/Array/Lemmas.lean b/Batteries/Data/Array/Lemmas.lean
@@ -153,8 +153,6 @@ theorem mapM_empty [Monad m] (f : α → m β) : mapM f #[] = pure #[] := by
 
 /-! ### mem -/
 
-alias not_mem_empty := not_mem_nil
-
 theorem mem_singleton : a ∈ #[b] ↔ a = b := by simp
 
 /-! ### append -/