Commit 2026-10-29 21:19 237c53b7

View on Github →

feat(LinearAlgebra/MultilinearMap): notation for MultilinearMap (#43877) Introduces the notation (Π i, M i) →ₗₘ[R] N for MultilinearMap R M N and (I → M) →ₗₘ[R] N for MultilinearMap R (fun _ : I => M) N, mirroring the notation M →ₗ[R] N for LinearMap R M N. Closes #43855.

Estimated changes

Modified Mathlib/Analysis/Calculus/ContDiff/FaaDiBruno.lean

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

modified theorem MultilinearMap.bound_of_shell

modified theorem MultilinearMap.bound_of_shell_of_continuous

modified theorem MultilinearMap.bound_of_shell_of_norm_map_coord_zero

modified theorem MultilinearMap.coe_mkContinuous

modified theorem MultilinearMap.continuous_of_bound

modified theorem MultilinearMap.exists_bound_of_continuous

modified def MultilinearMap.mkContinuous

modified def MultilinearMap.mkContinuousLinear

modified theorem MultilinearMap.mkContinuousLinear_norm_le'

modified theorem MultilinearMap.mkContinuousLinear_norm_le

modified def MultilinearMap.mkContinuousMultilinear

modified theorem MultilinearMap.mkContinuousMultilinear_apply

modified theorem MultilinearMap.mkContinuousMultilinear_norm_le'

modified theorem MultilinearMap.mkContinuousMultilinear_norm_le

modified theorem MultilinearMap.mkContinuous_norm_le'

modified theorem MultilinearMap.mkContinuous_norm_le

modified theorem MultilinearMap.norm_image_sub_le_of_bound'

modified theorem MultilinearMap.norm_image_sub_le_of_bound

modified theorem MultilinearMap.norm_map_coord_zero

modified theorem MultilinearMap.restr_norm_le

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

Modified Mathlib/LinearAlgebra/Alternating/Basic.lean

modified theorem AlternatingMap.coe_domDomCongr

modified theorem AlternatingMap.coe_mk

modified theorem AlternatingMap.coe_multilinearMap

modified theorem AlternatingMap.mk_zero

modified def AlternatingMap.toMultilinearMapLM

modified theorem AlternatingMap.toMultilinearMap_add

modified theorem AlternatingMap.toMultilinearMap_neg

modified theorem AlternatingMap.toMultilinearMap_smul

modified theorem AlternatingMap.toMultilinearMap_sub

modified theorem AlternatingMap.toMultilinearMap_zero

modified structure AlternatingMap

modified theorem LinearMap.compMultilinearMap_alternatization

modified def MultilinearMap.alternatization

modified theorem MultilinearMap.alternatization_apply

modified theorem MultilinearMap.alternatization_coe

modified theorem MultilinearMap.alternatization_compLinearMap

modified theorem MultilinearMap.alternatization_def

Modified Mathlib/LinearAlgebra/Alternating/DomCoprod.lean

Modified Mathlib/LinearAlgebra/Multilinear/Basic.lean

modified theorem LinearMap.add_compMultilinearMap

modified theorem LinearMap.coe_compMultilinearMap

modified def LinearMap.compMultilinearMap

modified theorem LinearMap.compMultilinearMap_add

modified theorem LinearMap.compMultilinearMap_apply

modified theorem LinearMap.compMultilinearMap_codRestrict

modified theorem LinearMap.compMultilinearMap_domDomCongr

modified theorem LinearMap.comp_compMultilinearMap

modified theorem LinearMap.id_compMultilinearMap

modified theorem LinearMap.subtype_compMultilinearMap_codRestrict

modified theorem LinearMap.zero_compMultilinearMap

modified def MultilinearMap.codRestrict

modified theorem MultilinearMap.coe_inj

modified theorem MultilinearMap.coe_injective

modified theorem MultilinearMap.coe_mk

modified theorem MultilinearMap.coe_restrictScalars

modified def MultilinearMap.compLinearMap

modified theorem MultilinearMap.compLinearMap_apply

modified theorem MultilinearMap.compLinearMap_assoc

modified theorem MultilinearMap.compLinearMap_id

modified def MultilinearMap.compMultilinearMap

modified theorem MultilinearMap.comp_linearEquiv_eq_zero_iff

modified theorem MultilinearMap.congr_fun

modified theorem MultilinearMap.cons_add

modified theorem MultilinearMap.cons_smul

modified def MultilinearMap.constLinearEquivOfIsEmpty

modified def MultilinearMap.constOfIsEmpty

modified def MultilinearMap.domDomCongr

modified def MultilinearMap.domDomCongrEquiv

modified theorem MultilinearMap.domDomCongr_eq_iff

modified theorem MultilinearMap.domDomCongr_mul

modified theorem MultilinearMap.domDomCongr_trans

modified def MultilinearMap.domDomRestrict

modified theorem MultilinearMap.domDomRestrict_apply

modified def MultilinearMap.domDomRestrictₗ

modified theorem MultilinearMap.ext

modified theorem MultilinearMap.ext_ring

modified def MultilinearMap.linearDeriv

modified theorem MultilinearMap.linearDeriv_apply

modified def MultilinearMap.map

modified theorem MultilinearMap.map_insertNth_add

modified theorem MultilinearMap.map_insertNth_smul

modified theorem MultilinearMap.map_nonempty

modified theorem MultilinearMap.mkPiRing_apply_one_eq_self

modified theorem MultilinearMap.mk_coe

modified def MultilinearMap.ofSubsingleton

modified def MultilinearMap.ofSubsingletonₗ

modified def MultilinearMap.prod

modified def MultilinearMap.range

modified def MultilinearMap.restr

modified def MultilinearMap.restrictScalars

modified def MultilinearMap.smulRight

modified theorem MultilinearMap.smulRight_apply

modified theorem MultilinearMap.snoc_add

modified theorem MultilinearMap.snoc_smul

Modified Mathlib/LinearAlgebra/Multilinear/Basis.lean

modified theorem Module.Basis.ext_multilinear

Modified Mathlib/LinearAlgebra/Multilinear/Curry.lean

modified theorem LinearMap.curry_uncurryLeft

modified def LinearMap.uncurryLeft

modified theorem LinearMap.uncurryLeft_apply

modified def LinearMap.uncurryMid

modified theorem MultilinearMap.curryFinFinset_symm_apply

modified def MultilinearMap.curryLeft

modified theorem MultilinearMap.curryLeft_apply

modified def MultilinearMap.curryMid

modified def MultilinearMap.curryRight

modified theorem MultilinearMap.curryRight_apply

modified def MultilinearMap.currySum

modified def MultilinearMap.currySumEquiv

modified theorem MultilinearMap.currySum_add

modified theorem MultilinearMap.currySum_apply

modified theorem MultilinearMap.currySum_smul

modified theorem MultilinearMap.currySum_uncurrySum

modified theorem MultilinearMap.uncurryMid_curryMid

modified def MultilinearMap.uncurryRight

modified def MultilinearMap.uncurrySum

modified theorem MultilinearMap.uncurrySum_add

modified theorem MultilinearMap.uncurrySum_apply

modified theorem MultilinearMap.uncurrySum_currySum

modified theorem MultilinearMap.uncurrySum_smul

modified theorem MultilinearMap.uncurry_curryLeft

modified theorem MultilinearMap.uncurry_curryRight

Modified Mathlib/LinearAlgebra/Multilinear/DFinsupp.lean

modified def MultilinearMap.dfinsuppFamily

modified theorem MultilinearMap.dfinsuppFamily_add

modified theorem MultilinearMap.dfinsupp_ext

modified theorem MultilinearMap.fromDFinsuppEquiv_apply

modified theorem MultilinearMap.fromDFinsuppEquiv_symm_apply

Modified Mathlib/LinearAlgebra/Multilinear/DirectSum.lean

Modified Mathlib/LinearAlgebra/Multilinear/FiniteDimensional.lean

Modified Mathlib/LinearAlgebra/Multilinear/Finsupp.lean

Modified Mathlib/LinearAlgebra/Multilinear/Pi.lean

modified def MultilinearMap.piFamily

modified theorem MultilinearMap.piFamily_add

modified theorem MultilinearMap.piFamily_zero

Modified Mathlib/LinearAlgebra/Multilinear/TensorProduct.lean

modified theorem MultilinearMap.domCoprod'_apply

modified def MultilinearMap.domCoprod

modified theorem MultilinearMap.domCoprodDep'_apply

modified def MultilinearMap.domCoprodDep

modified theorem MultilinearMap.domCoprod_domDomCongr_sumCongr

Modified Mathlib/LinearAlgebra/PiTensorProduct/Basic.lean

modified def PiTensorProduct.lift

modified theorem PiTensorProduct.liftAux.smul

modified def PiTensorProduct.liftAux

modified theorem PiTensorProduct.liftAux_tprod

modified theorem PiTensorProduct.liftAux_tprodCoeff

modified theorem PiTensorProduct.lift_comp_map

modified theorem PiTensorProduct.lift_comp_reindex

modified theorem PiTensorProduct.lift_comp_reindex_symm

modified theorem PiTensorProduct.lift_reindex

modified theorem PiTensorProduct.lift_reindex_symm

modified theorem PiTensorProduct.lift_tprod

modified def PiTensorProduct.tprod

modified theorem PiTensorProduct.tprod_eq_tprodCoeff_one

Modified Mathlib/LinearAlgebra/PiTensorProduct/Generators.lean

Modified Mathlib/LinearAlgebra/TensorAlgebra/Basic.lean

modified def TensorAlgebra.tprod

Modified Mathlib/LinearAlgebra/TensorPower/Pairing.lean

Modified Mathlib/LinearAlgebra/TensorPower/Symmetric.lean

modified def SymmetricPower.tprod

Modified Mathlib/RingTheory/PiTensorProduct.lean

modified def PiTensorProduct.liftAlgHom

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

modified def ContinuousMultilinearMap.toMultilinearMapLinear

Created MathlibTest/LinearAlgebra/Multilinear.lean