add classical

leanprover-community · Sep 20, 2024 · 57fce93 · 57fce93
1 parent 054ea42
commit 57fce93
Showing 1 changed file with 1 addition and 0 deletions.
diff --git a/Mathlib/RingTheory/MvPowerSeries/PiTopology.lean b/Mathlib/RingTheory/MvPowerSeries/PiTopology.lean
@@ -134,6 +134,7 @@ theorem continuous_C [Ring R] [TopologicalRing R] :
 
 theorem variables_tendsto_zero [Semiring R] :
     Filter.Tendsto (X · : σ → MvPowerSeries σ R) Filter.cofinite (nhds 0) := by
+  classical
   rw [tendsto_pi_nhds]
   simp_rw [apply_eq_coeff]
   intro d s hs