Commit 2022-08-09 21:53 511caf6a
View on Github →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.