Commit 2025-05-12 20:08 e9c4e6ad

View on Github →

feat(*Multilinear): add curryMid etc (#24798)

Estimated changes

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

added theorem ContinuousLinearMap.curryMid_uncurryMid

added theorem ContinuousLinearMap.norm_map_removeNth_le

added theorem ContinuousLinearMap.norm_uncurryMid

added def ContinuousLinearMap.uncurryMid

added def ContinuousMultilinearMap.curryMid

added def ContinuousMultilinearMap.curryMidEquiv

added theorem ContinuousMultilinearMap.curryMid_apply

added theorem ContinuousMultilinearMap.norm_curryMid

added theorem ContinuousMultilinearMap.norm_map_insertNth_le

added theorem ContinuousMultilinearMap.uncurryMid_curryMid

Modified Mathlib/Data/Fin/Tuple/Basic.lean

added theorem Fin.insertNth_update

added theorem Fin.removeNth_update_succAbove

Modified Mathlib/LinearAlgebra/Multilinear/Basic.lean

added theorem MultilinearMap.map_insertNth_add

added theorem MultilinearMap.map_insertNth_smul

Modified Mathlib/LinearAlgebra/Multilinear/Curry.lean

added theorem LinearMap.curryMid_uncurryMid

added def LinearMap.uncurryMid

added def MultilinearMap.curryMid

added def MultilinearMap.curryMidLinearEquiv

added theorem MultilinearMap.uncurryMid_curryMid