Commit 2025-01-16 07:31 ad0b8831

View on Github →

feat: replace statement that specific functions are C^ω by the fact that they are C^n for all n (#20769) This is equivalent mathematically, but in applications the latter form is often more convenient. For instance, when proving that the composition is C^n, it's better to have right away the fact that the function is C^n.

Estimated changes

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

modified theorem contDiff_prodAssoc

modified theorem contDiff_prodAssoc_symm

Modified Mathlib/Analysis/Complex/UpperHalfPlane/Manifold.lean

modified theorem UpperHalfPlane.contMDiffAt_ofComplex

modified theorem UpperHalfPlane.contMDiff_coe

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

modified theorem contDiffOn_stereoToFun

modified theorem contDiff_stereoInvFunAux

modified theorem contMDiff_circleExp

modified theorem contMDiff_coe_sphere

modified theorem contMDiff_neg_sphere

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