Commit 2025-09-28 11:30 5903cc2c

View on Github →

chore: move differentiability results about products to SpecificFunction (#30049) They are not used further in this file, and SpecificFunctions is specifically meant to contain their material.

Estimated changes

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

deleted theorem HasMFDerivAt.prodMk

deleted theorem HasMFDerivWithinAt.prodMk

deleted theorem MDifferentiable.prodMk

deleted theorem MDifferentiable.prodMk_space

deleted theorem MDifferentiableAt.prodMk

deleted theorem MDifferentiableAt.prodMk_space

deleted theorem MDifferentiableOn.prodMk

deleted theorem MDifferentiableOn.prodMk_space

deleted theorem MDifferentiableWithinAt.prodMk

deleted theorem MDifferentiableWithinAt.prodMk_space

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

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

added theorem HasMFDerivAt.prodMk

added theorem HasMFDerivWithinAt.prodMk

added theorem MDifferentiable.prodMk

added theorem MDifferentiable.prodMk_space

added theorem MDifferentiableAt.prodMk

added theorem MDifferentiableAt.prodMk_space

added theorem MDifferentiableOn.prodMk

added theorem MDifferentiableOn.prodMk_space

added theorem MDifferentiableWithinAt.prodMk

added theorem MDifferentiableWithinAt.prodMk_space