Theorem HasFiniteFPowerSeriesOnBall.mk'

Modification history

2025-02-20 08:08

Mathlib/Analysis/Analytic/CPolynomial.lean

chore: split CPolynomial (#22102) …

Modified HasFiniteFPowerSeriesOnBall.mk'View on Github →

2024-02-06 18:38

Mathlib/Analysis/Analytic/CPolynomial.lean

feat: define `ContinuousMultilinearMap.linearDeriv` and show it's the `fderiv` (#9846)

Added HasFiniteFPowerSeriesOnBall.mk'View on Github →