why not bundle it too

leanprover-community · Oct 18, 2024 · 02370cc · 02370cc
1 parent 69f1798
commit 02370cc
Showing 1 changed file with 13 additions and 0 deletions.
diff --git 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