Mathlib Changelog
v4
Changelog
About
Github
Commit
2025-02-26 07:29
d6d30b23
View on Github →
chore: split the long file
ContDiff.Basic
into two files (
#22293
)
Estimated changes
Modified
Mathlib.lean
Modified
Mathlib/Analysis/Analytic/IteratedFDeriv.lean
Modified
Mathlib/Analysis/Calculus/AddTorsor/AffineMap.lean
Modified
Mathlib/Analysis/Calculus/BumpFunction/Basic.lean
Modified
Mathlib/Analysis/Calculus/ContDiff/Basic.lean
deleted
theorem
ContDiff.add
deleted
theorem
ContDiff.const_smul
deleted
theorem
ContDiff.div
deleted
theorem
ContDiff.div_const
deleted
theorem
ContDiff.inv
deleted
theorem
ContDiff.mul
deleted
theorem
ContDiff.neg
deleted
theorem
ContDiff.pow
deleted
theorem
ContDiff.prod_map
deleted
theorem
ContDiff.restrict_scalars
deleted
theorem
ContDiff.smul
deleted
theorem
ContDiff.sub
deleted
theorem
ContDiff.sum
deleted
theorem
ContDiffAt.add
deleted
theorem
ContDiffAt.const_smul
deleted
theorem
ContDiffAt.neg
deleted
theorem
ContDiffAt.prod_map'
deleted
theorem
ContDiffAt.prod_map
deleted
theorem
ContDiffAt.restrict_scalars
deleted
theorem
ContDiffAt.smul
deleted
theorem
ContDiffAt.sub
deleted
theorem
ContDiffAt.sum
deleted
theorem
ContDiffOn.add
deleted
theorem
ContDiffOn.const_smul
deleted
theorem
ContDiffOn.div
deleted
theorem
ContDiffOn.div_const
deleted
theorem
ContDiffOn.inv
deleted
theorem
ContDiffOn.mul
deleted
theorem
ContDiffOn.neg
deleted
theorem
ContDiffOn.pow
deleted
theorem
ContDiffOn.prod_map
deleted
theorem
ContDiffOn.restrict_scalars
deleted
theorem
ContDiffOn.smul
deleted
theorem
ContDiffOn.sub
deleted
theorem
ContDiffOn.sum
deleted
theorem
ContDiffWithinAt.add
deleted
theorem
ContDiffWithinAt.const_smul
deleted
theorem
ContDiffWithinAt.div
deleted
theorem
ContDiffWithinAt.div_const
deleted
theorem
ContDiffWithinAt.inv
deleted
theorem
ContDiffWithinAt.mul
deleted
theorem
ContDiffWithinAt.neg
deleted
theorem
ContDiffWithinAt.pow
deleted
theorem
ContDiffWithinAt.prod_map'
deleted
theorem
ContDiffWithinAt.prod_map
deleted
theorem
ContDiffWithinAt.restrict_scalars
deleted
theorem
ContDiffWithinAt.smul
deleted
theorem
ContDiffWithinAt.sub
deleted
theorem
ContDiffWithinAt.sum
deleted
theorem
ContinuousLinearMap.IsInvertible.contDiffAt_map_inverse
deleted
theorem
HasFTaylorSeriesUpToOn.add
deleted
theorem
HasFTaylorSeriesUpToOn.restrictScalars
deleted
theorem
Homeomorph.contDiff_symm
deleted
theorem
Homeomorph.contDiff_symm_deriv
deleted
theorem
PartialHomeomorph.contDiffAt_symm
deleted
theorem
PartialHomeomorph.contDiffAt_symm_deriv
deleted
theorem
PartialHomeomorph.contDiffOn_restrContDiff_source
deleted
theorem
PartialHomeomorph.contDiffOn_restrContDiff_target
deleted
def
PartialHomeomorph.restrContDiff
deleted
theorem
contDiffAt_inv
deleted
theorem
contDiffAt_map_inverse
deleted
theorem
contDiffAt_pi
deleted
theorem
contDiffAt_prod'
deleted
theorem
contDiffAt_prod
deleted
theorem
contDiffAt_ring_inverse
deleted
theorem
contDiffOn_inv
deleted
theorem
contDiffOn_pi
deleted
theorem
contDiffOn_prod'
deleted
theorem
contDiffOn_prod
deleted
theorem
contDiffWithinAt_pi
deleted
theorem
contDiffWithinAt_prod'
deleted
theorem
contDiffWithinAt_prod
deleted
theorem
contDiff_add
deleted
theorem
contDiff_apply
deleted
theorem
contDiff_apply_apply
deleted
theorem
contDiff_const_smul
deleted
theorem
contDiff_mul
deleted
theorem
contDiff_neg
deleted
theorem
contDiff_pi
deleted
theorem
contDiff_prod'
deleted
theorem
contDiff_prod
deleted
theorem
contDiff_prod_mk_left
deleted
theorem
contDiff_prod_mk_right
deleted
theorem
contDiff_single
deleted
theorem
contDiff_smul
deleted
theorem
contDiff_update
deleted
theorem
hasFTaylorSeriesUpToOn_pi'
deleted
theorem
hasFTaylorSeriesUpToOn_pi
deleted
theorem
iteratedFDerivWithin_add_apply'
deleted
theorem
iteratedFDerivWithin_add_apply
deleted
theorem
iteratedFDerivWithin_const_smul_apply
deleted
theorem
iteratedFDerivWithin_neg_apply
deleted
theorem
iteratedFDerivWithin_sum_apply
deleted
theorem
iteratedFDeriv_add_apply'
deleted
theorem
iteratedFDeriv_add_apply
deleted
theorem
iteratedFDeriv_const_smul_apply'
deleted
theorem
iteratedFDeriv_const_smul_apply
deleted
theorem
iteratedFDeriv_neg_apply
deleted
theorem
iteratedFDeriv_sum
Modified
Mathlib/Analysis/Calculus/ContDiff/Bounds.lean
Modified
Mathlib/Analysis/Calculus/ContDiff/FiniteDimension.lean
Created
Mathlib/Analysis/Calculus/ContDiff/Operations.lean
added
theorem
ContDiff.add
added
theorem
ContDiff.const_smul
added
theorem
ContDiff.div
added
theorem
ContDiff.div_const
added
theorem
ContDiff.inv
added
theorem
ContDiff.mul
added
theorem
ContDiff.neg
added
theorem
ContDiff.pow
added
theorem
ContDiff.prod_map
added
theorem
ContDiff.restrict_scalars
added
theorem
ContDiff.smul
added
theorem
ContDiff.sub
added
theorem
ContDiff.sum
added
theorem
ContDiffAt.add
added
theorem
ContDiffAt.const_smul
added
theorem
ContDiffAt.neg
added
theorem
ContDiffAt.prod_map'
added
theorem
ContDiffAt.prod_map
added
theorem
ContDiffAt.restrict_scalars
added
theorem
ContDiffAt.smul
added
theorem
ContDiffAt.sub
added
theorem
ContDiffAt.sum
added
theorem
ContDiffOn.add
added
theorem
ContDiffOn.const_smul
added
theorem
ContDiffOn.div
added
theorem
ContDiffOn.div_const
added
theorem
ContDiffOn.inv
added
theorem
ContDiffOn.mul
added
theorem
ContDiffOn.neg
added
theorem
ContDiffOn.pow
added
theorem
ContDiffOn.prod_map
added
theorem
ContDiffOn.restrict_scalars
added
theorem
ContDiffOn.smul
added
theorem
ContDiffOn.sub
added
theorem
ContDiffOn.sum
added
theorem
ContDiffWithinAt.add
added
theorem
ContDiffWithinAt.const_smul
added
theorem
ContDiffWithinAt.div
added
theorem
ContDiffWithinAt.div_const
added
theorem
ContDiffWithinAt.inv
added
theorem
ContDiffWithinAt.mul
added
theorem
ContDiffWithinAt.neg
added
theorem
ContDiffWithinAt.pow
added
theorem
ContDiffWithinAt.prod_map'
added
theorem
ContDiffWithinAt.prod_map
added
theorem
ContDiffWithinAt.restrict_scalars
added
theorem
ContDiffWithinAt.smul
added
theorem
ContDiffWithinAt.sub
added
theorem
ContDiffWithinAt.sum
added
theorem
ContinuousLinearMap.IsInvertible.contDiffAt_map_inverse
added
theorem
HasFTaylorSeriesUpToOn.add
added
theorem
HasFTaylorSeriesUpToOn.restrictScalars
added
theorem
Homeomorph.contDiff_symm
added
theorem
Homeomorph.contDiff_symm_deriv
added
theorem
PartialHomeomorph.contDiffAt_symm
added
theorem
PartialHomeomorph.contDiffAt_symm_deriv
added
theorem
PartialHomeomorph.contDiffOn_restrContDiff_source
added
theorem
PartialHomeomorph.contDiffOn_restrContDiff_target
added
def
PartialHomeomorph.restrContDiff
added
theorem
contDiffAt_inv
added
theorem
contDiffAt_map_inverse
added
theorem
contDiffAt_pi
added
theorem
contDiffAt_prod'
added
theorem
contDiffAt_prod
added
theorem
contDiffAt_ring_inverse
added
theorem
contDiffOn_inv
added
theorem
contDiffOn_pi
added
theorem
contDiffOn_prod'
added
theorem
contDiffOn_prod
added
theorem
contDiffWithinAt_pi
added
theorem
contDiffWithinAt_prod'
added
theorem
contDiffWithinAt_prod
added
theorem
contDiff_add
added
theorem
contDiff_apply
added
theorem
contDiff_apply_apply
added
theorem
contDiff_const_smul
added
theorem
contDiff_mul
added
theorem
contDiff_neg
added
theorem
contDiff_pi
added
theorem
contDiff_prod'
added
theorem
contDiff_prod
added
theorem
contDiff_prod_mk_left
added
theorem
contDiff_prod_mk_right
added
theorem
contDiff_single
added
theorem
contDiff_smul
added
theorem
contDiff_update
added
theorem
hasFTaylorSeriesUpToOn_pi'
added
theorem
hasFTaylorSeriesUpToOn_pi
added
theorem
iteratedFDerivWithin_add_apply'
added
theorem
iteratedFDerivWithin_add_apply
added
theorem
iteratedFDerivWithin_const_smul_apply
added
theorem
iteratedFDerivWithin_neg_apply
added
theorem
iteratedFDerivWithin_sum_apply
added
theorem
iteratedFDeriv_add_apply'
added
theorem
iteratedFDeriv_add_apply
added
theorem
iteratedFDeriv_const_smul_apply'
added
theorem
iteratedFDeriv_const_smul_apply
added
theorem
iteratedFDeriv_neg_apply
added
theorem
iteratedFDeriv_sum
Modified
Mathlib/Analysis/Calculus/ContDiff/WithLp.lean
Modified
Mathlib/Analysis/Calculus/InverseFunctionTheorem/ContDiff.lean
Modified
Mathlib/Analysis/Calculus/IteratedDeriv/Lemmas.lean
Modified
Mathlib/Analysis/Calculus/SmoothSeries.lean
Modified
Mathlib/Analysis/Complex/RealDeriv.lean
Modified
Mathlib/Analysis/SpecialFunctions/Sqrt.lean
Modified
Mathlib/Geometry/Manifold/IsManifold/Basic.lean