Commit 2026-10-13 11:38 a646a376

View on Github →

feat: alternating maps and associated operations are ContMDiff and MDifferentiable (#44371) We follow the API already developed for continuous linear maps. These are prerequisites for the fact that differential forms are a smooth bundle.

Estimated changes

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

added theorem contMDiffAt_apply

added theorem contMDiffAt_pi_iff

added theorem contMDiffAt_pi_module_iff

deleted theorem contMDiffAt_pi_space

added theorem contMDiffOn_apply

added theorem contMDiffOn_pi_iff

added theorem contMDiffOn_pi_module_iff

deleted theorem contMDiffOn_pi_space

added theorem contMDiffWithinAt_apply

added theorem contMDiffWithinAt_pi_iff

added theorem contMDiffWithinAt_pi_module_iff

deleted theorem contMDiffWithinAt_pi_space

added theorem contMDiff_apply

added theorem contMDiff_pi_iff

added theorem contMDiff_pi_module_iff

deleted theorem contMDiff_pi_space

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

added theorem ContMDiff.compContinuousAlternatingMapCLM

added theorem ContMDiff.compContinuousLinearMapCLM

added theorem ContMDiff.continuousAlternatingMapCongr

added theorem ContMDiff.continuousAlternatingMap_apply

added theorem ContMDiffAt.compContinuousAlternatingMapCLM

added theorem ContMDiffOn.compContinuousAlternatingMapCLM

added theorem ContMDiffOn.compContinuousLinearMapCLM

added theorem ContMDiffOn.continuousAlternatingMapCongr

added theorem ContMDiffOn.continuousAlternatingMap_apply

added theorem ContMDiffWithinAt.compContinuousAlternatingMapCLM

added theorem ContMDiffWithinAt.compContinuousLinearMapCLM

added theorem ContMDiffWithinAt.continuousAlternatingMapCongr

added theorem ContMDiffWithinAt.continuousAlternatingMap_apply

added theorem ContinuousAlternatingMap.contMDiff

added theorem ContinuousAlternatingMap.contMDiffAt

added theorem ContinuousAlternatingMap.contMDiffOn

added theorem ContinuousAlternatingMap.contMDiffWithinAt

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

added theorem ContinuousAlternatingMap.mdifferentiable

added theorem ContinuousAlternatingMap.mdifferentiableAt

added theorem ContinuousAlternatingMap.mdifferentiableOn

added theorem ContinuousAlternatingMap.mdifferentiableWithinAt

added theorem MDifferentiable.compContinuousAlternatingMapCLM

added theorem MDifferentiable.compContinuousLinearMapCLM

added theorem MDifferentiable.continuousAlternatingMapCongr

added theorem MDifferentiable.continuousAlternatingMap_apply

added theorem MDifferentiableAt.compContinuousAlternatingMapCLM

added theorem MDifferentiableOn.compContinuousAlternatingMapCLM

added theorem MDifferentiableOn.compContinuousLinearMapCLM

added theorem MDifferentiableOn.continuousAlternatingMapCongr

added theorem MDifferentiableOn.continuousAlternatingMap_apply

added theorem MDifferentiableWithinAt.compContinuousAlternatingMapCLM

added theorem MDifferentiableWithinAt.compContinuousLinearMapCLM

added theorem MDifferentiableWithinAt.continuousAlternatingMapCongr

added theorem MDifferentiableWithinAt.continuousAlternatingMap_apply

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

added theorem mdifferentiableAt_apply

added theorem mdifferentiableAt_pi_iff

added theorem mdifferentiableAt_pi_space

added theorem mdifferentiableOn_apply

added theorem mdifferentiableOn_pi_iff

added theorem mdifferentiableOn_pi_space_iff

added theorem mdifferentiableWithinAt_apply

added theorem mdifferentiableWithinAt_pi_iff

added theorem mdifferentiableWithinAt_pi_space

added theorem mdifferentiable_apply

added theorem mdifferentiable_pi_iff

added theorem mdifferentiable_pi_space_iff

Modified Mathlib/Geometry/Manifold/WhitneyEmbedding.lean