Commit 2021-11-22 18:50 317483a6

feat(analysis/calculus/parametric_integral): generalize, rename (#10397)

• add integral to lemma names;
• a bit more general has_fderiv_at_integral_of_dominated_loc_of_lip': only require an estimate on ∥F x a - F x₀ a∥ instead of ∥F x a - F y a∥;
• generalize the deriv lemmas to F : 𝕜 → α → E, [is_R_or_C 𝕜].