From 02370cc8f9dd0bb88883814ad8b9a25d7fff2dcc Mon Sep 17 00:00:00 2001 From: Eric Wieser Date: Fri, 18 Oct 2024 23:50:24 +0000 Subject: [PATCH] why not bundle it too --- Mathlib/LinearAlgebra/Multilinear/Basic.lean | 13 +++++++++++++ 1 file changed, 13 insertions(+) diff --git a/Mathlib/LinearAlgebra/Multilinear/Basic.lean b/Mathlib/LinearAlgebra/Multilinear/Basic.lean index d51708c559b42..144320ca1178d 100644 --- a/Mathlib/LinearAlgebra/Multilinear/Basic.lean +++ b/Mathlib/LinearAlgebra/Multilinear/Basic.lean @@ -865,6 +865,19 @@ instance : Module S (MultilinearMap R M₁ M₂) := instance [NoZeroSMulDivisors S M₂] : NoZeroSMulDivisors S (MultilinearMap R M₁ M₂) := coe_injective.noZeroSMulDivisors _ rfl coe_smul +variable [AddCommMonoid M₃] [Module S M₃] [Module R M₃] [SMulCommClass R S M₃] + +variable (S) in +/-- `LinearMap.compMultilinearMap` as an `S`-linear map. -/ +@[simps] +def _root_.LinearMap.compMultilinearMapₗ [Semiring S] [Module S M₂] [Module S M₃] + [SMulCommClass R S M₂] [SMulCommClass R S M₃] [LinearMap.CompatibleSMul M₂ M₃ S R] + (g : M₂ →ₗ[R] M₃) : + MultilinearMap R M₁ M₂ →ₗ[S] MultilinearMap R M₁ M₃ where + toFun := g.compMultilinearMap + map_add' := g.compMultilinearMap_add + map_smul' := g.compMultilinearMap_smul + variable (R S M₁ M₂ M₃) section OfSubsingleton