Commit 2025-03-03 16:46 f555fdaa

View on Github →

chore(Data/Set): rename *prod_mk* -> *prodMk* (#22190)

Estimated changes

Modified Mathlib/Analysis/BoxIntegral/Basic.lean

Modified Mathlib/Analysis/Calculus/BumpFunction/FiniteDimension.lean

Modified Mathlib/Analysis/Calculus/ContDiff/Basic.lean

Modified Mathlib/Analysis/Calculus/MeanValue.lean

Modified Mathlib/Analysis/Convolution.lean

Modified Mathlib/Analysis/SpecialFunctions/PolarCoord.lean

Modified Mathlib/Data/Prod/TProd.lean

Modified Mathlib/Data/Set/Operations.lean

added theorem Set.prodMk_mem_set_prod_eq

deleted theorem Set.prod_mk_mem_set_prod_eq

Modified Mathlib/Data/Set/Prod.lean

added theorem Set.image_prodMk_subset_prod

added theorem Set.image_prodMk_subset_prod_left

added theorem Set.image_prodMk_subset_prod_right

deleted theorem Set.image_prod_mk_subset_prod

deleted theorem Set.image_prod_mk_subset_prod_left

deleted theorem Set.image_prod_mk_subset_prod_right

Modified Mathlib/Logic/Equiv/Set.lean

Modified Mathlib/MeasureTheory/Integral/SetIntegral.lean

Modified Mathlib/MeasureTheory/Measure/Prod.lean

Modified Mathlib/ModelTheory/Syntax.lean

Modified Mathlib/Probability/Kernel/Composition/CompProd.lean

Modified Mathlib/Probability/Kernel/Disintegration/CDFToKernel.lean

Modified Mathlib/Topology/Algebra/UniformGroup/Basic.lean

Modified Mathlib/Topology/FiberBundle/Basic.lean

Modified Mathlib/Topology/FiberBundle/Constructions.lean

Modified Mathlib/Topology/FiberBundle/Trivialization.lean