Commit 2025-01-19 11:52 23742102

View on Github →

feat: remove UniqueDiffWithinAt assumptions for one-dimensional derivative (#20816) A point in a subset of a field is either a point of unique differentials, or isolated. In both cases, there is a definite value for the derivative of a map (its unique derivative in the former case, zero in the latter case). This means there is no choice involved, contrary to what happens in higher dimension. This remark means we can remove many UniqueDiffWithinAt assumptions in one-dimensional settings.

Estimated changes

modified theorem derivWithin.neg
modified theorem derivWithin_add
modified theorem derivWithin_add_const
modified theorem derivWithin_const_add
modified theorem derivWithin_const_sub
modified theorem derivWithin_sub
modified theorem derivWithin_sub_const
modified theorem derivWithin_sum
modified theorem derivWithin_inv'
modified theorem derivWithin_clm_apply
modified theorem derivWithin_const_mul
modified theorem derivWithin_const_smul
modified theorem derivWithin_div_const
modified theorem derivWithin_finset_prod
modified theorem derivWithin_mul
modified theorem derivWithin_mul_const
modified theorem derivWithin_smul
modified theorem derivWithin_smul_const
modified theorem derivWithin_pow'
modified theorem derivWithin_pi
modified theorem iteratedDerivWithin_one
modified theorem iteratedDerivWithin_succ'
modified theorem iteratedDerivWithin_succ