Commit 2025-10-09 08:14 67f5eec6

View on Github →

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

Estimated changes

Modified Mathlib/Analysis/Analytic/CPolynomial.lean

added theorem ContinuousMultilinearMap.analyticAt_uncurry_compContinuousLinearMap

added theorem ContinuousMultilinearMap.analyticAt_uncurry_of_linear

added theorem ContinuousMultilinearMap.analyticOnNhd_uncurry_compContinuousLinearMap

added theorem ContinuousMultilinearMap.analyticOnNhd_uncurry_of_linear

added theorem ContinuousMultilinearMap.analyticOn_uncurry_compContinuousLinearMap

added theorem ContinuousMultilinearMap.analyticOn_uncurry_of_linear

added theorem ContinuousMultilinearMap.analyticWithinAt_uncurry_compContinuousLinearMap

added theorem ContinuousMultilinearMap.analyticWithinAt_uncurry_of_linear

added theorem ContinuousMultilinearMap.cpolynomialAt_uncurry_compContinuousLinearMap

added theorem ContinuousMultilinearMap.cpolynomialAt_uncurry_of_linear

added theorem ContinuousMultilinearMap.cpolynomialOn_uncurry_compContinuousLinearMap

added theorem ContinuousMultilinearMap.cpolyomialOn_uncurry_of_linear

Modified Mathlib/Analysis/NormedSpace/Multilinear/Basic.lean

added theorem ContinuousLinearMap.coe_flipMultilinearEquiv

added theorem ContinuousLinearMap.coe_symm_flipMultilinearEquiv

added theorem ContinuousLinearMap.flipLinear_flipMultilinear

added def ContinuousLinearMap.flipMultilinearEquiv

added def ContinuousLinearMap.flipMultilinearEquivₗ

added def ContinuousMultilinearMap.flipLinear

added theorem ContinuousMultilinearMap.flipMultilinear_flipLinear