Commit 2025-03-08 19:41 02a95579

View on Github →

chore(Geometry/Manifold): rename many lemmas (#22719) Mostly from prod_mk to prodMk. Cherry-picked from #22195

Estimated changes

Modified Mathlib/Geometry/Manifold/Algebra/LieGroup.lean

Modified Mathlib/Geometry/Manifold/Algebra/Monoid.lean

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

added theorem ContMDiff.prodMap

added theorem ContMDiff.prodMk_space

deleted theorem ContMDiff.prod_map

deleted theorem ContMDiff.prod_mk_space

added theorem ContMDiffAt.prodMap'

added theorem ContMDiffAt.prodMap

deleted theorem ContMDiffAt.prod_map'

deleted theorem ContMDiffAt.prod_map

added theorem ContMDiffOn.prodMap

added theorem ContMDiffOn.prodMk

added theorem ContMDiffOn.prodMk_space

deleted theorem ContMDiffOn.prod_map

deleted theorem ContMDiffOn.prod_mk

deleted theorem ContMDiffOn.prod_mk_space

added theorem ContMDiffWithinAt.prodMap'

added theorem ContMDiffWithinAt.prodMap

added theorem ContMDiffWithinAt.prodMk

added theorem ContMDiffWithinAt.prodMk_space

deleted theorem ContMDiffWithinAt.prod_map'

deleted theorem ContMDiffWithinAt.prod_map

deleted theorem ContMDiffWithinAt.prod_mk

deleted theorem ContMDiffWithinAt.prod_mk_space

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

Modified Mathlib/Geometry/Manifold/ContMDiffMFDeriv.lean

Modified Mathlib/Geometry/Manifold/ContMDiffMap.lean

Modified Mathlib/Geometry/Manifold/Diffeomorph.lean

Modified Mathlib/Geometry/Manifold/Instances/Sphere.lean

Modified Mathlib/Geometry/Manifold/Instances/UnitsOfNormedAlgebra.lean

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

added theorem MDifferentiable.prodMk

added theorem MDifferentiable.prodMk_space

deleted theorem MDifferentiable.prod_mk

deleted theorem MDifferentiable.prod_mk_space

added theorem MDifferentiableAt.prodMk

added theorem MDifferentiableAt.prodMk_space

deleted theorem MDifferentiableAt.prod_mk

deleted theorem MDifferentiableAt.prod_mk_space

added theorem MDifferentiableOn.prodMk

added theorem MDifferentiableOn.prodMk_space

deleted theorem MDifferentiableOn.prod_mk

deleted theorem MDifferentiableOn.prod_mk_space

added theorem MDifferentiableWithinAt.prodMk

added theorem MDifferentiableWithinAt.prodMk_space

deleted theorem MDifferentiableWithinAt.prod_mk

deleted theorem MDifferentiableWithinAt.prod_mk_space

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

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

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

Modified Mathlib/Geometry/Manifold/WhitneyEmbedding.lean