Def FormalMultilinearSeries.derivSeries

Modification history

2024-09-17 19:29

Mathlib/Analysis/Analytic/Basic.lean

chore: split the `change origin` part from `Analytic.Basic` (#16891) …

Modified FormalMultilinearSeries.derivSeries View on Github →

2024-02-01 09:38

Mathlib/Analysis/Analytic/Basic.lean

feat(Analysis.Calculus.FDeriv.Analytic + Analysis.Complex.TaylorSeries): Taylor series of holomorphic functions (#10087) …

Added FormalMultilinearSeries.derivSeries View on Github →