Laurent

leanprover-community · Oct 1, 2024 · 1f13179 · 1f13179
1 parent f7a8f88
commit 1f13179
Showing 1 changed file with 1 addition and 1 deletion.
diff --git a/Mathlib/RingTheory/LaurentSeries.lean b/Mathlib/RingTheory/LaurentSeries.lean
@@ -771,7 +771,7 @@ theorem Cauchy.eventually_mem_nhds {ℱ : Filter (LaurentSeries K)} (hℱ : Cauc
     rw [← WithZero.coe_unzero γ.ne_zero, WithZero.coe_lt_coe, hD₀, neg_neg, ofAdd_sub,
       ofAdd_toAdd, div_lt_comm, div_self', ← ofAdd_zero, Multiplicative.ofAdd_lt]
     exact zero_lt_one
-  apply coeff_eventually_equal hℱ |>.mono
+  apply coeff_eventually_equal (D := D) hℱ |>.mono
   intro _ hf
   apply lt_of_le_of_lt (valuation_le_iff_coeff_lt_eq_zero K |>.mpr _) hD
   intro n hn