remove bogus deprecated alias

leanprover-community · Oct 9, 2024 · f3b25b6 · f3b25b6
1 parent e5f13fc
commit f3b25b6
Showing 1 changed file with 0 additions and 3 deletions.
diff --git a/Mathlib/Data/ENat/Lattice.lean b/Mathlib/Data/ENat/Lattice.lean
@@ -209,9 +209,6 @@ lemma finsetSum_iSup_of_monotone {α ι : Type*} [Preorder ι] [IsDirected ι (
     {f : α → ι → ℕ∞} (hf : ∀ a, Monotone (f a)) : (∑ a ∈ s, iSup (f a)) = ⨆ n, ∑ a ∈ s, f a n :=
   finsetSum_iSup fun i j ↦ (exists_ge_ge i j).imp fun _k ⟨hi, hj⟩ a ↦ ⟨hf a hi, hf a hj⟩
 
-@[deprecated (since := "2024-07-14")]
-alias finset_sum_iSup_nat := finsetSum_iSup_of_monotone
-
 proof_wanted smul_iSup {R} [SMul R ℕ∞] [IsScalarTower R ℕ∞ ℕ∞] (f : ι → ℕ∞) (c : R) :
     c • ⨆ i, f i = ⨆ i, c • f i