Mathlib Changelog
v4
Changelog
About
Github
Theorem
ContinuousMultilinearMap.analyticWithinAt_uncurry_of_linear
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.analyticWithinAt_uncurry_of_linear
View on Github →