refactor(LinearAlgebra/BilinearMap): Left composition, bilinear over different rings (#13042)

Generalise `compl₂` and `compl₁₂` for left composition with maps which are linear over different rings in the first and second variable.

Needed for #9334



Co-authored-by: Christopher Hoskin <mans0954@users.noreply.github.com>

Author: mans0954

Mathlib/LinearAlgebra/BilinearMap.lean

@@ -325,8 +325,14 @@ end
 
 /-- Composing a linear map `Q → N` and a bilinear map `M → N → P` to
 form a bilinear map `M → Q → P`. -/
-def compl₂ (g : Q →ₛₗ[σ₄₂] N) : M →ₛₗ[σ₁₃] Q →ₛₗ[σ₄₃] P :=
-  (lcompₛₗ _ _ g).comp f
+def compl₂ {R₅ : Type*} [CommSemiring R₅] [Module R₅ P] [SMulCommClass R₃ R₅ P] {σ₁₅ : R →+* R₅}
+    (h : M →ₛₗ[σ₁₅] N →ₛₗ[σ₂₃] P) (g : Q →ₛₗ[σ₄₂] N) : M →ₛₗ[σ₁₅] Q →ₛₗ[σ₄₃] P where
+  toFun a := (lcompₛₗ P σ₂₃ g) (h a)
+  map_add' _ _ := by
+    simp [map_add]
+  map_smul' _ _ := by
+    simp only [LinearMap.map_smulₛₗ, lcompₛₗ]
+    rfl
 #align linear_map.compl₂ LinearMap.compl₂
 
 @[simp]
@@ -341,8 +347,10 @@ theorem compl₂_id : f.compl₂ LinearMap.id = f := by
 
 /-- Composing linear maps `Q → M` and `Q' → N` with a bilinear map `M → N → P` to
 form a bilinear map `Q → Q' → P`. -/
-def compl₁₂ (f : Mₗ →ₗ[R] Nₗ →ₗ[R] Pₗ) (g : Qₗ →ₗ[R] Mₗ) (g' : Qₗ' →ₗ[R] Nₗ) :
-    Qₗ →ₗ[R] Qₗ' →ₗ[R] Pₗ :=
+def compl₁₂ {R₁ : Type*} [CommSemiring R₁] [Module R₂ N] [Module R₂ Pₗ] [Module R₁ Pₗ]
+    [Module R₁ Mₗ] [SMulCommClass R₂ R₁ Pₗ] [Module R₁ Qₗ] [Module R₂ Qₗ']
+    (f : Mₗ →ₗ[R₁] N →ₗ[R₂] Pₗ) (g : Qₗ →ₗ[R₁] Mₗ) (g' : Qₗ' →ₗ[R₂] N) :
+    Qₗ →ₗ[R₁] Qₗ' →ₗ[R₂] Pₗ :=
   (f.comp g).compl₂ g'
 #align linear_map.compl₁₂ LinearMap.compl₁₂