Theorem ContinuousMultilinearMap.curry0_apply

Modification history

2026-10-13 19:23
Mathlib/Analysis/Normed/Module/Multilinear/Curry.lean
chore(Analysis/Normed): generalize `ContinuousMultilinearMap.curry0` to TVS (#44321) …
Modified ContinuousMultilinearMap.curry0_applyView on Github →
2025-03-13 02:38
Mathlib/Analysis/NormedSpace/Multilinear/Curry.lean
chore: whitespace again (#22878) …
Modified ContinuousMultilinearMap.curry0_applyView on Github →
2024-09-15 13:34
Mathlib/Analysis/NormedSpace/Multilinear/Curry.lean
fix: correct curry/uncurry confusion in (Continuous)MultilinearMap (#15530) …
Modified ContinuousMultilinearMap.curry0_applyView on Github →
2023-11-14 16:55
Mathlib/Analysis/NormedSpace/Multilinear.lean
chore: split Analysis.NormedSpace.Multilinear (#8392) …
Modified ContinuousMultilinearMap.curry0_applyView on Github →
2023-05-18 20:25
Mathlib/Analysis/NormedSpace/Multilinear.lean
feat: port Analysis.NormedSpace.Multilinear (#4057) …
Added ContinuousMultilinearMap.curry0_applyView on Github →