Commit 2025-03-14 06:42 65468c4b

View on Github →

chore: review of erw in Topology/ (#22914)

Estimated changes

Modified Mathlib/Data/Set/Prod.lean

Modified Mathlib/Topology/Algebra/InfiniteSum/Constructions.lean

added theorem tprod_prod_uncurry

Modified Mathlib/Topology/Algebra/UniformField.lean

Modified Mathlib/Topology/Compactness/Compact.lean

Modified Mathlib/Topology/ContinuousMap/StoneWeierstrass.lean

Modified Mathlib/Topology/Instances/AddCircle.lean

Modified Mathlib/Topology/Instances/Complex.lean

Modified Mathlib/Topology/SeparatedMap.lean

Modified Mathlib/Topology/Separation/Basic.lean