fixed long line

leanprover-community · Oct 29, 2024 · adaff80 · adaff80
1 parent aee8446
commit adaff80
Showing 1 changed file with 0 additions and 1 deletion.
diff --git a/Mathlib/RingTheory/LaurentSeries.lean b/Mathlib/RingTheory/LaurentSeries.lean
@@ -48,7 +48,6 @@ series to which the filter `ℱ` converges.
 `LaurentSeries.val_le_one_iff_eq_coe`.
 * The uniform space of `LaurentSeries` over a field is complete, formalized in the instance
 `instLaurentSeriesComplete`.
-************************************************************************************************************************
 * The field of rational functions is dense in `LaurentSeries`: this is the declaration
 `LaurentSeries.coe_range_dense` and relies principally upon `LaurentSeries.exists_ratFunc_val_lt`,
 stating that for every Laurent series `f` and every `γ : ℤₘ₀` one can find a rational function `Q`