Commit 2026-07-27 17:36 024a9ab3

View on Github →

chore(Geometry/Manifold): fix defs with underscores (#42115) This PR deprecates all definitions in differential geometry with underscores in their names, and renames it according to the naming convention.

Estimated changes

Modified Mathlib/Geometry/Manifold/ChartedSpace.lean

added def ChartedSpace.ofDiscreteTopology

deleted def ChartedSpace.of_discreteTopology

added def ChartedSpace.sumOfNonempty

deleted def ChartedSpace.sum_of_nonempty

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

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

added theorem CovariantDerivative.ContMDiffCovariantDerivative.affineCombination

deleted theorem CovariantDerivative.ContMDiffCovariantDerivative.affine_combination

added theorem CovariantDerivative.ContMDiffCovariantDerivative.finiteAffineCombination

deleted theorem CovariantDerivative.ContMDiffCovariantDerivative.finite_affine_combination

added def CovariantDerivative.affineCombination

deleted def CovariantDerivative.affine_combination

added def CovariantDerivative.finiteAffineCombination

deleted def CovariantDerivative.finite_affine_combination

added def CovariantDerivative.ofIsCovariantDerivativeOnOfOpenCover

deleted def CovariantDerivative.of_isCovariantDerivativeOn_of_open_cover

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

added theorem Bundle.Trivialization.eq_sum_localFrameCoeff_smul

deleted theorem Bundle.Trivialization.eq_sum_localFrame_coeff_smul

added def Bundle.Trivialization.localFrameCoeff

added theorem Bundle.Trivialization.localFrameCoeff_apply_of_mem_baseSet

added theorem Bundle.Trivialization.localFrameCoeff_apply_of_notMem_baseSet

added theorem Bundle.Trivialization.localFrameCoeff_congr

added theorem Bundle.Trivialization.localFrameCoeff_eq_coeff

deleted def Bundle.Trivialization.localFrame_coeff

deleted theorem Bundle.Trivialization.localFrame_coeff_apply_of_mem_baseSet

deleted theorem Bundle.Trivialization.localFrame_coeff_apply_of_notMem_baseSet

deleted theorem Bundle.Trivialization.localFrame_coeff_congr

deleted theorem Bundle.Trivialization.localFrame_coeff_eq_coeff

added theorem contMDiffAt_iff_localFrameCoeff

deleted theorem contMDiffAt_iff_localFrame_coeff

added theorem contMDiffAt_localFrameCoeff

deleted theorem contMDiffAt_localFrame_coeff

added theorem contMDiffOn_baseSet_iff_localFrameCoeff

deleted theorem contMDiffOn_baseSet_iff_localFrame_coeff

added theorem contMDiffOn_baseSet_localFrameCoeff

deleted theorem contMDiffOn_baseSet_localFrame_coeff

added theorem contMDiffOn_iff_localFrameCoeff

deleted theorem contMDiffOn_iff_localFrame_coeff

added theorem contMDiffOn_localFrameCoeff

deleted theorem contMDiffOn_localFrame_coeff

added theorem mdifferentiableAt_iff_localFrameCoeff

deleted theorem mdifferentiableAt_iff_localFrame_coeff

added theorem mdifferentiableAt_localFrameCoeff

deleted theorem mdifferentiableAt_localFrame_coeff

added theorem mdifferentiableOn_baseSet_localFrameCoeff

deleted theorem mdifferentiableOn_baseSet_localFrame_coeff

added theorem mdifferentiableOn_localFrameCoeff

deleted theorem mdifferentiableOn_localFrame_coeff

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