Commit 2025-02-26 07:29 d6d30b23

View on Github →

chore: split the long file ContDiff.Basic into two files (#22293)

Estimated changes

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.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.smul
deleted theorem ContDiffOn.sub
deleted theorem ContDiffOn.sum
deleted theorem ContDiffWithinAt.add
deleted theorem ContDiffWithinAt.div
deleted theorem ContDiffWithinAt.inv
deleted theorem ContDiffWithinAt.mul
deleted theorem ContDiffWithinAt.neg
deleted theorem ContDiffWithinAt.pow
deleted theorem ContDiffWithinAt.prod_map
deleted theorem ContDiffWithinAt.smul
deleted theorem ContDiffWithinAt.sub
deleted theorem ContDiffWithinAt.sum
deleted theorem Homeomorph.contDiff_symm
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 iteratedFDeriv_add_apply'
deleted theorem iteratedFDeriv_add_apply
deleted theorem iteratedFDeriv_neg_apply
deleted theorem iteratedFDeriv_sum
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.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.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.smul
added theorem ContDiffOn.sub
added theorem ContDiffOn.sum
added theorem ContDiffWithinAt.add
added theorem ContDiffWithinAt.div
added theorem ContDiffWithinAt.inv
added theorem ContDiffWithinAt.mul
added theorem ContDiffWithinAt.neg
added theorem ContDiffWithinAt.pow
added theorem ContDiffWithinAt.smul
added theorem ContDiffWithinAt.sub
added theorem ContDiffWithinAt.sum
added theorem contDiffAt_inv
added theorem contDiffAt_map_inverse
added theorem contDiffAt_pi
added theorem contDiffAt_prod'
added theorem contDiffAt_prod
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 iteratedFDeriv_sum