Theorem FormalMultilinearSeries.ofScalars_sub

Modification history

2025-12-10 16:38

Mathlib/Analysis/Analytic/OfScalars.lean

feat(Analysis): `HasFPowerSeriesOnBall (fun x ↦ 1 / (1 - x))` and friends (#32373)

Added FormalMultilinearSeries.ofScalars_sub View on Github →