Commit 2026-10-13 19:23 9492379e

View on Github →

chore(Analysis/Normed): generalize ContinuousMultilinearMap.curry0 to TVS (#44321) Move and generalize the definition and basic properties of curry0 and uncurry0 to topological space. Needed to generalize iterated derivatives to TVS.

Estimated changes

Modified Mathlib/Analysis/Normed/Module/Multilinear/Curry.lean

deleted theorem ContinuousMultilinearMap.apply_zero_uncurry0

deleted def ContinuousMultilinearMap.curry0

deleted theorem ContinuousMultilinearMap.curry0_apply

deleted theorem ContinuousMultilinearMap.curry0_uncurry0

deleted def ContinuousMultilinearMap.uncurry0

deleted theorem ContinuousMultilinearMap.uncurry0_apply

deleted theorem ContinuousMultilinearMap.uncurry0_curry0

Modified Mathlib/Topology/Algebra/Module/Multilinear/Basic.lean

added theorem ContinuousMultilinearMap.apply_zero_uncurry0

added def ContinuousMultilinearMap.curry0

added theorem ContinuousMultilinearMap.curry0_apply

added theorem ContinuousMultilinearMap.curry0_uncurry0

added def ContinuousMultilinearMap.uncurry0

added theorem ContinuousMultilinearMap.uncurry0_apply

added theorem ContinuousMultilinearMap.uncurry0_curry0