Commit 2025-04-11 02:53 e6de4eaf

View on Github →

chore: rename Set.range_prod_map -> Set.range_prodMap (#23925)

Estimated changes

Modified Mathlib/Data/Set/Prod.lean

added theorem Set.range_prodMap

deleted theorem Set.range_prod_map

Modified Mathlib/Geometry/Manifold/ContMDiffMFDeriv.lean

Modified Mathlib/Geometry/Manifold/IsManifold/InteriorBoundary.lean

Modified Mathlib/MeasureTheory/MeasurableSpace/Prod.lean

Modified Mathlib/NumberTheory/LSeries/PrimesInAP.lean

Modified Mathlib/Topology/UniformSpace/Basic.lean

Modified Mathlib/Topology/UniformSpace/Equicontinuity.lean