Commit 2024-06-19 11:32 b6c1b896

View on Github →

feat: add a few analytic function lemmas for future AnalyticManifold use (#13784) This is a few isolated lemmas split out of https://github.com/leanprover-community/mathlib4/pull/10853.

  1. AnalyticAt.comp_of_eq
  2. FormalMultilinearSeries.zero_radius
  3. constFormalMultilinearSeries_zero

Estimated changes

added theorem AnalyticAt.comp_of_eq