Def ContinuousLinearMap.fpowerSeries

Modification history

2023-10-18 11:36

Mathlib/Analysis/Analytic/Linear.lean

feat(Analysis/Analytic): some more API for analytic functions (#7552) …

Modified ContinuousLinearMap.fpowerSeries View on Github →

2023-06-02 11:07

Mathlib/Analysis/Analytic/Linear.lean

feat: port Analysis.Analytic.Linear (#4566)

Added ContinuousLinearMap.fpowerSeries View on Github →