Commit 2026-03-05 11:23 4877fdaa

View on Github →

chore(Geometry/Manifold/MFDeriv/SpecificFunctions): golf using custom… (#36009) … elaborators

Estimated changes

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

modified theorem ContinuousLinearEquiv.mfderiv_eq

modified theorem ContinuousLinearMap.mfderivWithin_eq

modified theorem ContinuousLinearMap.mfderiv_eq

modified theorem HasMFDerivAt.add

modified theorem HasMFDerivAt.const_smul

modified theorem HasMFDerivAt.neg

modified theorem HasMFDerivAt.sub

modified theorem HasMFDerivAt.sum

modified theorem HasMFDerivWithinAt.add

modified theorem HasMFDerivWithinAt.neg

modified theorem HasMFDerivWithinAt.sum

modified theorem MDifferentiable.add

modified theorem MDifferentiable.const_smul

modified theorem MDifferentiable.fst

modified theorem MDifferentiable.neg

modified theorem MDifferentiable.prodMap

modified theorem MDifferentiable.prodMk

modified theorem MDifferentiable.prodMk_space

modified theorem MDifferentiable.snd

modified theorem MDifferentiable.sub

modified theorem MDifferentiable.sum

modified theorem MDifferentiableAt.add

modified theorem MDifferentiableAt.const_smul

modified theorem MDifferentiableAt.fst

modified theorem MDifferentiableAt.neg

modified theorem MDifferentiableAt.prodMap'

modified theorem MDifferentiableAt.prodMap

modified theorem MDifferentiableAt.prodMk

modified theorem MDifferentiableAt.snd

modified theorem MDifferentiableAt.sub

modified theorem MDifferentiableAt.sum

modified theorem MDifferentiableOn.add

modified theorem MDifferentiableOn.neg

modified theorem MDifferentiableOn.prodMap

modified theorem MDifferentiableOn.prodMk

modified theorem MDifferentiableOn.sum

modified theorem MDifferentiableWithinAt.add

modified theorem MDifferentiableWithinAt.neg

modified theorem MDifferentiableWithinAt.prodMap'

modified theorem MDifferentiableWithinAt.prodMap

modified theorem MDifferentiableWithinAt.snd

modified theorem const_smul_mfderiv

modified theorem hasMFDerivAt_neg

modified theorem mdifferentiableAt_const

modified theorem mdifferentiableAt_fst

modified theorem mdifferentiableAt_id

modified theorem mdifferentiableAt_neg

modified theorem mdifferentiableAt_snd

modified theorem mdifferentiableOn_const

modified theorem mdifferentiableOn_fst

modified theorem mdifferentiableOn_id

modified theorem mdifferentiableOn_snd

modified theorem mdifferentiableWithinAt_const

modified theorem mdifferentiableWithinAt_id

modified theorem mdifferentiable_const

modified theorem mdifferentiable_fst

modified theorem mdifferentiable_id

modified theorem mdifferentiable_snd

modified theorem mfderivWithin_prodMk

modified theorem mfderiv_add

modified theorem mfderiv_id

modified theorem mfderiv_neg

modified theorem mfderiv_prodMk

modified theorem mfderiv_prod_eq_add_comp

modified theorem mfderiv_sub