Theorem ContinuousMultilinearMap.flipMultilinear_flipLinear

Modification history

2025-10-09 08:14
Mathlib/Analysis/NormedSpace/Multilinear/Basic.lean
feat: composing a continuous multilinear map with continuous linear maps is analytic in both variables (#30111)
Added ContinuousMultilinearMap.flipMultilinear_flipLinearView on Github →