mathlib

511caf6a - chore(analysis/calculus/cont_diff): rename and add @[simp] to `iterated_fderiv_within_zero_fun` (#15896)

chore(analysis/calculus/cont_diff): rename and add @[simp] to `iterated_fderiv_within_zero_fun` (#15896) Rename the lemma `iterated_fderiv_within_zero_fun` to `iterated_fderiv_zero_fun` because it is not stated with `iterated_fderiv_within` and add the `simp` attribute.