Commit 2025-03-10 12:58 606847f7

View on Github →

chore(Analysis): rename many lemmas (#22737)

prod/prod_mk -> prodMk
prod_map -> prodMap

Estimated changes

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

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

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

deleted theorem ContDiff.prod

added theorem ContDiff.prodMk

deleted theorem ContDiffAt.prod

added theorem ContDiffAt.prodMk

deleted theorem ContDiffOn.prod

added theorem ContDiffOn.prodMk

deleted theorem ContDiffWithinAt.prod

added theorem ContDiffWithinAt.prodMk

deleted theorem HasFTaylorSeriesUpToOn.prod

added theorem HasFTaylorSeriesUpToOn.prodMk

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

added theorem ContDiff.prodMap

deleted theorem ContDiff.prod_map

added theorem ContDiffAt.prodMap'

added theorem ContDiffAt.prodMap

deleted theorem ContDiffAt.prod_map'

deleted theorem ContDiffAt.prod_map

added theorem ContDiffOn.prodMap

deleted theorem ContDiffOn.prod_map

added theorem ContDiffWithinAt.prodMap'

added theorem ContDiffWithinAt.prodMap

deleted theorem ContDiffWithinAt.prod_map'

deleted theorem ContDiffWithinAt.prod_map

added theorem contDiff_prodMk_left

added theorem contDiff_prodMk_right

deleted theorem contDiff_prod_mk_left

deleted theorem contDiff_prod_mk_right

Modified Mathlib/Analysis/Calculus/Deriv/Prod.lean

Modified Mathlib/Analysis/Calculus/FDeriv/Analytic.lean

Modified Mathlib/Analysis/Calculus/FDeriv/Bilinear.lean

Modified Mathlib/Analysis/Calculus/FDeriv/Mul.lean

Modified Mathlib/Analysis/Calculus/FDeriv/Prod.lean

deleted theorem Differentiable.prod

added theorem Differentiable.prodMk

deleted theorem DifferentiableAt.fderiv_prod

added theorem DifferentiableAt.fderiv_prodMk

deleted theorem DifferentiableAt.prod

added theorem DifferentiableAt.prodMk

deleted theorem DifferentiableOn.prod

added theorem DifferentiableOn.prodMk

deleted theorem DifferentiableWithinAt.fderivWithin_prod

added theorem DifferentiableWithinAt.fderivWithin_prodMk

deleted theorem DifferentiableWithinAt.prod

added theorem DifferentiableWithinAt.prodMk

deleted theorem HasFDerivAtFilter.prod

added theorem HasFDerivAtFilter.prodMk

added theorem hasFDerivAt_prodMk_left

added theorem hasFDerivAt_prodMk_right

deleted theorem hasFDerivAt_prod_mk_left

deleted theorem hasFDerivAt_prod_mk_right

Modified Mathlib/Analysis/Calculus/Implicit.lean

Modified Mathlib/Analysis/Calculus/LagrangeMultipliers.lean

Modified Mathlib/Analysis/Convolution.lean

Modified Mathlib/Analysis/Distribution/SchwartzSpace.lean

Modified Mathlib/Analysis/InnerProductSpace/Calculus.lean

Modified Mathlib/Analysis/SpecialFunctions/PolarCoord.lean

Modified Mathlib/Analysis/SpecialFunctions/Pow/Deriv.lean

Modified Mathlib/Geometry/Manifold/ContMDiff/Constructions.lean

Modified Mathlib/Geometry/Manifold/ContMDiffMFDeriv.lean

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

Modified Mathlib/Geometry/Manifold/MFDeriv/Basic.lean

Modified Mathlib/Geometry/Manifold/MFDeriv/SpecificFunctions.lean

Modified Mathlib/NumberTheory/ModularForms/JacobiTheta/TwoVariable.lean