Commit 2023-06-02 11:07 be7e0e9b

View on Github →

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

Estimated changes

Modified Mathlib.lean

Created Mathlib/Analysis/Analytic/Linear.lean

added def ContinuousLinearMap.fpowerSeries

added def ContinuousLinearMap.fpowerSeriesBilinear

added theorem ContinuousLinearMap.fpowerSeriesBilinear_radius

added theorem ContinuousLinearMap.fpowerSeries_apply_add_two

added theorem ContinuousLinearMap.fpowerSeries_radius

added def ContinuousLinearMap.uncurryBilinear

added theorem ContinuousLinearMap.uncurryBilinear_apply