restore StoneWeierstrass

leanprover-community · Feb 21, 2025 · a00977d · a00977d
1 parent 42d0007
commit a00977d
Show file tree

Hide file tree

Showing 2 changed files with 1 addition and 3 deletions.
diff --git a/Mathlib/Analysis/Calculus/FDeriv/MvPolynomial.lean b/Mathlib/Analysis/Calculus/FDeriv/MvPolynomial.lean
@@ -9,7 +9,6 @@ import Mathlib.Analysis.Calculus.FDeriv.Mul
 import Mathlib.Analysis.Calculus.Deriv.Pow
 import Mathlib.Algebra.BigOperators.Group.Finset
 
-
 /-!
 # Derivatives of multivariate polynomials
 

diff --git a/Mathlib/Topology/ContinuousMap/StoneWeierstrass.lean b/Mathlib/Topology/ContinuousMap/StoneWeierstrass.lean
@@ -7,7 +7,6 @@ import Mathlib.Analysis.RCLike.Basic
 import Mathlib.Topology.Algebra.StarSubalgebra
 import Mathlib.Topology.ContinuousMap.ContinuousMapZero
 import Mathlib.Topology.ContinuousMap.Weierstrass
-import Mathlib.Topology.ContinuousMap.MvPolynomial
 import Mathlib.Topology.ContinuousMap.Lattice
 
 /-!
@@ -435,7 +434,7 @@ section PolynomialFunctions
 open StarSubalgebra Polynomial
 open scoped Polynomial
 
-/-- Polynomial functions are dense in `C(s, ℝ)` when `s` is compact.
+/-- Polynomial functions in are dense in `C(s, ℝ)` when `s` is compact.
 
 See `polynomialFunctions_closure_eq_top` for the special case `s = Set.Icc a b` which does not use
 the full Stone-Weierstrass theorem. Of course, that version could be used to prove this one as
-Original file line number
+Diff line change
@@ Expand Up / @@ -9,7 +9,6 @@ import Mathlib.Analysis.Calculus.FDeriv.Mul @@
     import Mathlib.Analysis.Calculus.Deriv.Pow
     import Mathlib.Algebra.BigOperators.Group.Finset
     /-!
     # Derivatives of multivariate polynomials
@@ Expand Down @@