Commit 2026-10-17 10:55 035a8717

View on Github →

chore: rename toContinuousMap to ContinuousMap.ofClass (#44877) This is in line with #31365, and avoids shadowing names of concrete projections FooClass.toContinuousMap.

Estimated changes

Modified Mathlib/AlgebraicGeometry/IdealSheaf/Subscheme.lean

Modified Mathlib/Topology/Algebra/ContinuousAffineEquiv.lean

Modified Mathlib/Topology/ContinuousMap/Defs.lean

added def ContinuousMap.ofClass

deleted def toContinuousMap

Modified Mathlib/Topology/ContinuousMap/Ideals.lean

Modified Mathlib/Topology/ContinuousMap/StarOrdered.lean

Modified Mathlib/Topology/ContinuousMap/StoneWeierstrass.lean

Modified Mathlib/Topology/Homotopy/HomotopyGroup.lean

Modified Mathlib/Topology/Homotopy/Lifting.lean

Modified Mathlib/Topology/Homotopy/TopCat/Path.lean

Modified Mathlib/Topology/Homotopy/TopCat/ZerothHomotopy.lean

Modified Mathlib/Topology/UniformSpace/Path.lean