Theorem ContinuousMultilinearMap.cpolynomialAt_uncurry_compContinuousLinearMap

Modification history

2025-10-09 08:14

Mathlib/Analysis/Analytic/CPolynomial.lean

feat: composing a continuous multilinear map with continuous linear maps is analytic in both variables (#30111)

Added ContinuousMultilinearMap.cpolynomialAt_uncurry_compContinuousLinearMap View on Github →