diff --git a/Mathlib/LinearAlgebra/BilinearForm/Hom.lean b/Mathlib/LinearAlgebra/BilinearForm/Hom.lean
index 17f78fa9dc6ea..9c011c36ed52b 100644
--- a/Mathlib/LinearAlgebra/BilinearForm/Hom.lean
+++ b/Mathlib/LinearAlgebra/BilinearForm/Hom.lean
@@ -262,15 +262,8 @@ variable [AddCommMonoid M'] [AddCommMonoid M''] [Module R M'] [Module R M'']
 section congr
 
 /-- Apply a linear equivalence on the arguments of a bilinear form. -/
-def congr (e : M ≃ₗ[R] M') : BilinForm R M ≃ₗ[R] BilinForm R M' where
-  toFun B := B.comp e.symm e.symm
-  invFun B := B.comp e e
-  left_inv B := ext₂ fun x => by
-    simp only [comp_apply, LinearEquiv.coe_coe, LinearEquiv.symm_apply_apply, forall_const]
-  right_inv B := ext₂ fun x => by
-    simp only [comp_apply, LinearEquiv.coe_coe, LinearEquiv.apply_symm_apply, forall_const]
-  map_add' _ _ := ext₂ fun _ _ => rfl
-  map_smul' _ _ := ext₂ fun _ _ => rfl
+def congr (e : M ≃ₗ[R] M') : BilinForm R M ≃ₗ[R] BilinForm R M' :=
+  LinearEquiv.congrRight (LinearEquiv.congrLeft _ _ e) ≪≫ₗ LinearEquiv.congrLeft _ _ e
 
 @[simp]
 theorem congr_apply (e : M ≃ₗ[R] M') (B : BilinForm R M) (x y : M') :
diff --git a/Mathlib/LinearAlgebra/BilinearForm/TensorProduct.lean b/Mathlib/LinearAlgebra/BilinearForm/TensorProduct.lean
index d7ab301e16a91..5b0fb0f4e2877 100644
--- a/Mathlib/LinearAlgebra/BilinearForm/TensorProduct.lean
+++ b/Mathlib/LinearAlgebra/BilinearForm/TensorProduct.lean
@@ -5,6 +5,7 @@ Authors: Eric Wieser
 -/
 import Mathlib.LinearAlgebra.Dual
 import Mathlib.LinearAlgebra.TensorProduct.Tower
+import Mathlib.LinearAlgebra.BilinearForm.Hom
 
 /-!
 # The bilinear form on a tensor product
@@ -20,24 +21,69 @@ import Mathlib.LinearAlgebra.TensorProduct.Tower
 
 suppress_compilation
 
-universe u v w uι uR uA uM₁ uM₂
+universe u v w uι uR uA uM₁ uM₂ uN₁ uN₂
 
-variable {ι : Type uι} {R : Type uR} {A : Type uA} {M₁ : Type uM₁} {M₂ : Type uM₂}
+variable {ι : Type uι} {R : Type uR} {A : Type uA} {M₁ : Type uM₁} {M₂ : Type uM₂} {N₁ : Type uN₁}
+  {N₂ : Type uN₂}
 
 open TensorProduct
 
 namespace LinearMap
 
-namespace BilinMap
-
 open LinearMap (BilinMap BilinForm)
 
 section CommSemiring
+
 variable [CommSemiring R] [CommSemiring A]
-variable [AddCommMonoid M₁] [AddCommMonoid M₂]
-variable [Algebra R A] [Module R M₁] [Module A M₁]
+variable [AddCommMonoid M₁] [AddCommMonoid M₂] [AddCommMonoid N₁] [AddCommMonoid N₂]
+variable [Algebra R A] [Module R M₁] [Module A M₁] [Module R N₁] [Module A N₁]
 variable [SMulCommClass R A M₁] [IsScalarTower R A M₁]
-variable [Module R M₂]
+variable [SMulCommClass R A N₁] [IsScalarTower R A N₁]
+variable [Module R M₂] [Module R N₂]
+
+namespace BilinMap
+
+variable (R A) in
+/-- The tensor product of two bilinear maps injects into bilinear maps on tensor products.
+
+Note this is heterobasic; the bilinear map on the left can take values in a module over a
+(commutative) algebra over the ring of the module in which the right bilinear map is valued. -/
+def tensorDistrib :
+    (BilinMap A M₁ N₁ ⊗[R] BilinMap R M₂ N₂) →ₗ[A] BilinMap A (M₁ ⊗[R] M₂) (N₁ ⊗[R] N₂) :=
+  (TensorProduct.lift.equiv A (M₁ ⊗[R] M₂) (M₁ ⊗[R] M₂) (N₁ ⊗[R] N₂)).symm.toLinearMap ∘ₗ
+ ((LinearMap.llcomp A _ _ _).flip
+   (TensorProduct.AlgebraTensorModule.tensorTensorTensorComm R A M₁ M₂ M₁ M₂).toLinearMap)
+  ∘ₗ TensorProduct.AlgebraTensorModule.homTensorHomMap R _ _ _ _ _ _
+  ∘ₗ (TensorProduct.AlgebraTensorModule.congr
+    (TensorProduct.lift.equiv A M₁ M₁ N₁)
+    (TensorProduct.lift.equiv R _ _ _)).toLinearMap
+
+@[simp]
+theorem tensorDistrib_tmul (B₁ : BilinMap A M₁ N₁) (B₂ : BilinMap R M₂ N₂) (m₁ : M₁) (m₂ : M₂)
+    (m₁' : M₁) (m₂' : M₂) :
+    tensorDistrib R A (B₁ ⊗ₜ B₂) (m₁ ⊗ₜ m₂) (m₁' ⊗ₜ m₂')
+      = B₁ m₁ m₁' ⊗ₜ B₂ m₂ m₂' :=
+  rfl
+
+/-- The tensor product of two bilinear forms, a shorthand for dot notation. -/
+protected abbrev tmul (B₁ : BilinMap A M₁ N₁) (B₂ : BilinMap R M₂ N₂) :
+    BilinMap A (M₁ ⊗[R] M₂) (N₁ ⊗[R] N₂) :=
+  tensorDistrib R A (B₁ ⊗ₜ[R] B₂)
+
+variable (A) in
+/-- The base change of a bilinear map (also known as "extension of scalars"). -/
+protected def baseChange (B : BilinMap R M₂ N₂) : BilinMap A (A ⊗[R] M₂) (A ⊗[R] N₂) :=
+  BilinMap.tmul (R := R) (A := A) (M₁ := A) (M₂ := M₂) (LinearMap.mul A A) B
+
+@[simp]
+theorem baseChange_tmul (B₂ : BilinMap R M₂ N₂) (a : A) (m₂ : M₂)
+    (a' : A) (m₂' : M₂) :
+    B₂.baseChange A (a ⊗ₜ m₂) (a' ⊗ₜ m₂') = (a * a') ⊗ₜ (B₂ m₂ m₂')  :=
+  rfl
+
+end BilinMap
+
+namespace BilinForm
 
 variable (R A) in
 /-- The tensor product of two bilinear forms injects into bilinear forms on tensor products.
@@ -45,12 +91,9 @@ variable (R A) in
 Note this is heterobasic; the bilinear form on the left can take values in an (commutative) algebra
 over the ring in which the right bilinear form is valued. -/
 def tensorDistrib : BilinForm A M₁ ⊗[R] BilinForm R M₂ →ₗ[A] BilinForm A (M₁ ⊗[R] M₂) :=
-  ((TensorProduct.AlgebraTensorModule.tensorTensorTensorComm R A M₁ M₂ M₁ M₂).dualMap
-    ≪≫ₗ (TensorProduct.lift.equiv A (M₁ ⊗[R] M₂) (M₁ ⊗[R] M₂) A).symm).toLinearMap
-  ∘ₗ TensorProduct.AlgebraTensorModule.dualDistrib R _ _ _
-  ∘ₗ (TensorProduct.AlgebraTensorModule.congr
-    (TensorProduct.lift.equiv A M₁ M₁ A)
-    (TensorProduct.lift.equiv R _ _ _)).toLinearMap
+  (AlgebraTensorModule.rid R A A).congrRight₂.toLinearMap ∘ₗ (BilinMap.tensorDistrib R A)
+
+variable (R A) in
 
 -- TODO: make the RHS `MulOpposite.op (B₂ m₂ m₂') • B₁ m₁ m₁'` so that this has a nicer defeq for
 -- `R = A` of `B₁ m₁ m₁' * B₂ m₂ m₂'`, as it did before the generalization in #6306.
@@ -62,12 +105,12 @@ theorem tensorDistrib_tmul (B₁ : BilinForm A M₁) (B₂ : BilinForm R M₂) (
   rfl
 
 /-- The tensor product of two bilinear forms, a shorthand for dot notation. -/
-protected abbrev tmul (B₁ : BilinMap A M₁ A) (B₂ : BilinMap  R M₂ R) : BilinMap A (M₁ ⊗[R] M₂) A :=
+protected abbrev tmul (B₁ : BilinForm A M₁) (B₂ : BilinMap  R M₂ R) : BilinMap A (M₁ ⊗[R] M₂) A :=
   tensorDistrib R A (B₁ ⊗ₜ[R] B₂)
 
 attribute [local ext] TensorProduct.ext in
 /-- A tensor product of symmetric bilinear forms is symmetric. -/
-lemma _root_.LinearMap.IsSymm.tmul {B₁ : BilinMap A M₁ A} {B₂ : BilinMap R M₂ R}
+lemma _root_.LinearMap.IsSymm.tmul {B₁ : BilinForm A M₁} {B₂ : BilinForm R M₂}
     (hB₁ : B₁.IsSymm) (hB₂ : B₂.IsSymm) : (B₁.tmul B₂).IsSymm := by
   rw [LinearMap.isSymm_iff_eq_flip]
   ext x₁ x₂ y₁ y₂
@@ -75,11 +118,11 @@ lemma _root_.LinearMap.IsSymm.tmul {B₁ : BilinMap A M₁ A} {B₂ : BilinMap R
 
 variable (A) in
 /-- The base change of a bilinear form. -/
-protected def baseChange (B : BilinMap R M₂ R) : BilinForm A (A ⊗[R] M₂) :=
-  BilinMap.tmul (R := R) (A := A) (M₁ := A) (M₂ := M₂) (LinearMap.mul A A) B
+protected def baseChange (B : BilinForm R M₂) : BilinForm A (A ⊗[R] M₂) :=
+  BilinForm.tmul (R := R) (A := A) (M₁ := A) (M₂ := M₂) (LinearMap.mul A A) B
 
 @[simp]
-theorem baseChange_tmul (B₂ : BilinMap R M₂ R) (a : A) (m₂ : M₂)
+theorem baseChange_tmul (B₂ : BilinForm R M₂) (a : A) (m₂ : M₂)
     (a' : A) (m₂' : M₂) :
     B₂.baseChange A (a ⊗ₜ m₂) (a' ⊗ₜ m₂') = (B₂ m₂ m₂') • (a * a') :=
   rfl
@@ -89,6 +132,8 @@ variable (A) in
 lemma IsSymm.baseChange {B₂ : BilinForm R M₂} (hB₂ : B₂.IsSymm) : (B₂.baseChange A).IsSymm :=
   IsSymm.tmul mul_comm hB₂
 
+end BilinForm
+
 end CommSemiring
 
 section CommRing
@@ -99,6 +144,8 @@ variable [Module R M₁] [Module R M₂]
 variable [Module.Free R M₁] [Module.Finite R M₁]
 variable [Module.Free R M₂] [Module.Finite R M₂]
 
+namespace BilinForm
+
 variable (R) in
 /-- `tensorDistrib` as an equivalence. -/
 noncomputable def tensorDistribEquiv :
@@ -131,8 +178,8 @@ theorem tensorDistribEquiv_apply (B : BilinForm R M₁ ⊗ BilinForm R M₂) :
     tensorDistribEquiv R (M₁ := M₁) (M₂ := M₂) B = tensorDistrib R R B :=
   DFunLike.congr_fun (tensorDistribEquiv_toLinearMap R M₁ M₂) B
 
-end CommRing
+end BilinForm
 
-end BilinMap
+end CommRing
 
 end LinearMap
diff --git a/Mathlib/LinearAlgebra/CliffordAlgebra/BaseChange.lean b/Mathlib/LinearAlgebra/CliffordAlgebra/BaseChange.lean
index e83ba0a051353..e25b22b5361e7 100644
--- a/Mathlib/LinearAlgebra/CliffordAlgebra/BaseChange.lean
+++ b/Mathlib/LinearAlgebra/CliffordAlgebra/BaseChange.lean
@@ -95,7 +95,7 @@ noncomputable def toBaseChange (Q : QuadraticForm R V) :
       exact hpure_tensor v w
     intros v w
     rw [← TensorProduct.tmul_add, CliffordAlgebra.ι_mul_ι_add_swap,
-      QuadraticForm.polarBilin_baseChange, LinearMap.BilinMap.baseChange_tmul, one_mul,
+      QuadraticForm.polarBilin_baseChange, LinearMap.BilinForm.baseChange_tmul, one_mul,
       TensorProduct.smul_tmul, Algebra.algebraMap_eq_smul_one, QuadraticMap.polarBilin_apply_apply]
 
 @[simp] theorem toBaseChange_ι (Q : QuadraticForm R V) (z : A) (v : V) :
diff --git a/Mathlib/LinearAlgebra/QuadraticForm/Basic.lean b/Mathlib/LinearAlgebra/QuadraticForm/Basic.lean
index 0a53cfbd1d352..1ce6224fb182f 100644
--- a/Mathlib/LinearAlgebra/QuadraticForm/Basic.lean
+++ b/Mathlib/LinearAlgebra/QuadraticForm/Basic.lean
@@ -887,12 +887,12 @@ theorem toQuadraticMap_associated : (associatedHom S Q).toQuadraticMap = Q :=
 -- note: usually `rightInverse` lemmas are named the other way around, but this is consistent
 -- with historical naming in this file.
 theorem associated_rightInverse :
-    Function.RightInverse (associatedHom S) (BilinMap.toQuadraticMap : _ → QuadraticMap R M R) :=
+    Function.RightInverse (associatedHom S) (BilinMap.toQuadraticMap : _ → QuadraticMap R M N) :=
   fun Q => toQuadraticMap_associated S Q
 
 /-- `associated'` is the `ℤ`-linear map that sends a quadratic form on a module `M` over `R` to its
 associated symmetric bilinear form. -/
-abbrev associated' : QuadraticMap R M R →ₗ[ℤ] BilinMap R M R :=
+abbrev associated' : QuadraticMap R M N →ₗ[ℤ] BilinMap R M N :=
   associatedHom ℤ
 
 /-- Symmetric bilinear forms can be lifted to quadratic forms -/
@@ -902,15 +902,18 @@ instance canLift :
 
 /-- There exists a non-null vector with respect to any quadratic form `Q` whose associated
 bilinear form is non-zero, i.e. there exists `x` such that `Q x ≠ 0`. -/
-theorem exists_quadraticForm_ne_zero {Q : QuadraticForm R M}
+theorem exists_quadraticMap_ne_zero {Q : QuadraticMap R M N}
     -- Porting note: added implicit argument
-    (hB₁ : associated' (R := R) Q ≠ 0) :
+    (hB₁ : associated' (R := R) (N := N) Q ≠ 0) :
     ∃ x, Q x ≠ 0 := by
   rw [← not_forall]
   intro h
   apply hB₁
   rw [(QuadraticMap.ext h : Q = 0), LinearMap.map_zero]
 
+@[deprecated (since := "2024-10-05")] alias exists_quadraticForm_ne_zero :=
+  exists_quadraticMap_ne_zero
+
 end AssociatedHom
 
 section Associated
@@ -1037,7 +1040,7 @@ variable [CommRing R] [AddCommGroup M] [Module R M]
 theorem separatingLeft_of_anisotropic [Invertible (2 : R)] (Q : QuadraticMap R M R)
     (hB : Q.Anisotropic) :
     -- Porting note: added implicit argument
-    (QuadraticMap.associated' (R := R) Q).SeparatingLeft := fun x hx ↦ hB _ <| by
+    (QuadraticMap.associated' (R := R) (N := R) Q).SeparatingLeft := fun x hx ↦ hB _ <| by
   rw [← hx x]
   exact (associated_eq_self_apply _ _ x).symm
 
@@ -1194,7 +1197,7 @@ on a module `M` over a ring `R` with invertible `2`, i.e. there exists some
 theorem exists_bilinForm_self_ne_zero [htwo : Invertible (2 : R)] {B : BilinForm R M}
     (hB₁ : B ≠ 0) (hB₂ : B.IsSymm) : ∃ x, ¬B.IsOrtho x x := by
   lift B to QuadraticForm R M using hB₂ with Q
-  obtain ⟨x, hx⟩ := QuadraticMap.exists_quadraticForm_ne_zero hB₁
+  obtain ⟨x, hx⟩ := QuadraticMap.exists_quadraticMap_ne_zero hB₁
   exact ⟨x, fun h => hx (Q.associated_eq_self_apply ℕ x ▸ h)⟩
 
 open Module
diff --git a/Mathlib/LinearAlgebra/QuadraticForm/TensorProduct.lean b/Mathlib/LinearAlgebra/QuadraticForm/TensorProduct.lean
index 1d4c4ee3c081a..48cee02f8f77e 100644
--- a/Mathlib/LinearAlgebra/QuadraticForm/TensorProduct.lean
+++ b/Mathlib/LinearAlgebra/QuadraticForm/TensorProduct.lean
@@ -16,50 +16,77 @@ import Mathlib.LinearAlgebra.QuadraticForm.Basic
 
 -/
 
-universe uR uA uM₁ uM₂
+universe uR uA uM₁ uM₂ uN₁ uN₂
 
-variable {R : Type uR} {A : Type uA} {M₁ : Type uM₁} {M₂ : Type uM₂}
+variable {R : Type uR} {A : Type uA} {M₁ : Type uM₁} {M₂ : Type uM₂} {N₁ : Type uN₁} {N₂ : Type uN₂}
 
 open LinearMap (BilinMap BilinForm)
 open TensorProduct QuadraticMap
 
-namespace QuadraticForm
-
 section CommRing
 variable [CommRing R] [CommRing A]
-variable [AddCommGroup M₁] [AddCommGroup M₂]
-variable [Algebra R A] [Module R M₁] [Module A M₁]
-variable [SMulCommClass R A M₁] [IsScalarTower R A M₁]
-variable [Module R M₂]
+variable [AddCommGroup M₁] [AddCommGroup M₂] [AddCommGroup N₁] [AddCommGroup N₂]
+variable [Algebra R A] [Module R M₁] [Module A M₁] [Module R N₁] [Module A N₁]
+variable [SMulCommClass R A M₁] [IsScalarTower R A M₁] [SMulCommClass R A N₁] [IsScalarTower R A N₁]
+variable [Module R M₂] [Module R N₂]
 
 section InvertibleTwo
 variable [Invertible (2 : R)]
 
+namespace QuadraticMap
+
 variable (R A) in
-/-- The tensor product of two quadratic forms injects into quadratic forms on tensor products.
+/-- The tensor product of two quadratic maps injects into quadratic maps on tensor products.
 
-Note this is heterobasic; the quadratic form on the left can take values in a larger ring than
-the one on the right. -/
+Note this is heterobasic; the quadratic map on the left can take values in a module over a larger
+ring than the one on the right. -/
 -- `noncomputable` is a performance workaround for mathlib4#7103
 noncomputable def tensorDistrib :
-    QuadraticForm A M₁ ⊗[R] QuadraticForm R M₂ →ₗ[A] QuadraticForm A (M₁ ⊗[R] M₂) :=
+    QuadraticMap A M₁ N₁ ⊗[R] QuadraticMap R M₂ N₂ →ₗ[A] QuadraticMap A (M₁ ⊗[R] M₂) (N₁ ⊗[R] N₂) :=
   letI : Invertible (2 : A) := (Invertible.map (algebraMap R A) 2).copy 2 (map_ofNat _ _).symm
   -- while `letI`s would produce a better term than `let`, they would make this already-slow
   -- definition even slower.
   let toQ := BilinMap.toQuadraticMapLinearMap A A (M₁ ⊗[R] M₂)
   let tmulB := BilinMap.tensorDistrib R A (M₁ := M₁) (M₂ := M₂)
   let toB := AlgebraTensorModule.map
-      (QuadraticMap.associated : QuadraticForm A M₁ →ₗ[A] BilinForm A M₁)
-      (QuadraticMap.associated : QuadraticForm R M₂ →ₗ[R] BilinForm R M₂)
+      (QuadraticMap.associated : QuadraticMap A M₁ N₁ →ₗ[A] BilinMap A M₁ N₁)
+      (QuadraticMap.associated : QuadraticMap R M₂ N₂ →ₗ[R] BilinMap R M₂ N₂)
   toQ ∘ₗ tmulB ∘ₗ toB
 
+@[simp]
+theorem tensorDistrib_tmul (Q₁ : QuadraticMap A M₁ N₁) (Q₂ : QuadraticMap R M₂ N₂) (m₁ : M₁)
+    (m₂ : M₂) : tensorDistrib R A (Q₁ ⊗ₜ Q₂) (m₁ ⊗ₜ m₂) = Q₁ m₁ ⊗ₜ Q₂ m₂   :=
+  letI : Invertible (2 : A) := (Invertible.map (algebraMap R A) 2).copy 2 (map_ofNat _ _).symm
+  (BilinMap.tensorDistrib_tmul _ _ _ _ _ _).trans <| congr_arg₂ _
+    (associated_eq_self_apply _ _ _) (associated_eq_self_apply _ _ _)
+
+/-- The tensor product of two quadratic maps, a shorthand for dot notation. -/
+-- `noncomputable` is a performance workaround for mathlib4#7103
+protected noncomputable abbrev tmul (Q₁ : QuadraticMap A M₁ N₁)
+    (Q₂ : QuadraticMap R M₂ N₂) : QuadraticMap A (M₁ ⊗[R] M₂) (N₁ ⊗[R] N₂) :=
+  tensorDistrib R A (Q₁ ⊗ₜ[R] Q₂)
+
+end QuadraticMap
+
+namespace QuadraticForm
+
+variable (R A) in
+/-- The tensor product of two quadratic forms injects into quadratic forms on tensor products.
+
+Note this is heterobasic; the quadratic form on the left can take values in a larger ring than
+the one on the right. -/
+-- `noncomputable` is a performance workaround for mathlib4#7103
+noncomputable def tensorDistrib :
+    QuadraticForm A M₁ ⊗[R] QuadraticForm R M₂ →ₗ[A] QuadraticForm A (M₁ ⊗[R] M₂) :=
+  (AlgebraTensorModule.rid R A A).congrQuadraticMap.toLinearMap ∘ₗ QuadraticMap.tensorDistrib R A
+
 -- TODO: make the RHS `MulOpposite.op (Q₂ m₂) • Q₁ m₁` so that this has a nicer defeq for
 -- `R = A` of `Q₁ m₁ * Q₂ m₂`.
 @[simp]
 theorem tensorDistrib_tmul (Q₁ : QuadraticForm A M₁) (Q₂ : QuadraticForm R M₂) (m₁ : M₁) (m₂ : M₂) :
     tensorDistrib R A (Q₁ ⊗ₜ Q₂) (m₁ ⊗ₜ m₂) = Q₂ m₂ • Q₁ m₁ :=
   letI : Invertible (2 : A) := (Invertible.map (algebraMap R A) 2).copy 2 (map_ofNat _ _).symm
-  (BilinMap.tensorDistrib_tmul _ _ _ _ _ _).trans <| congr_arg₂ _
+  (LinearMap.BilinForm.tensorDistrib_tmul _ _ _ _ _ _ _ _).trans <| congr_arg₂ _
     (associated_eq_self_apply _ _ _) (associated_eq_self_apply _ _ _)
 
 /-- The tensor product of two quadratic forms, a shorthand for dot notation. -/
@@ -70,15 +97,29 @@ protected noncomputable abbrev tmul (Q₁ : QuadraticForm A M₁) (Q₂ : Quadra
 
 theorem associated_tmul [Invertible (2 : A)] (Q₁ : QuadraticForm A M₁) (Q₂ : QuadraticForm R M₂) :
     associated (R := A) (Q₁.tmul Q₂)
-      = (associated (R := A) Q₁).tmul (associated (R := R) Q₂) := by
-  rw [QuadraticForm.tmul, tensorDistrib, BilinMap.tmul]
+      = BilinForm.tmul ((associated (R := A) Q₁)) (associated (R := R) Q₂) := by
+  letI : Invertible (2 : A) := (Invertible.map (algebraMap R A) 2).copy 2 (map_ofNat _ _).symm
+  /- Previously `QuadraticForm.tensorDistrib` was defined in a similar way to
+  `QuadraticMap.tensorDistrib`. We now obtain the definition of `QuadraticForm.tensorDistrib`
+  from `QuadraticMap.tensorDistrib` using `A ⊗[R] R ≃ₗ[A] A`. Hypothesis `e1` below shows that the
+  new definition is equal to the old, and allows us to reuse the old proof.
+
+  TODO: Define `IsSymm` for bilinear maps and generalise this result to Quadratic Maps.
+  -/
+  have e1: (BilinMap.toQuadraticMapLinearMap A A (M₁ ⊗[R] M₂) ∘
+    BilinForm.tensorDistrib R A (M₁ := M₁) (M₂ := M₂) ∘
+    AlgebraTensorModule.map
+      (QuadraticMap.associated : QuadraticForm A M₁ →ₗ[A] BilinForm A M₁)
+      (QuadraticMap.associated : QuadraticForm R M₂ →ₗ[R] BilinForm R M₂)) =
+       tensorDistrib R A := rfl
+  rw [QuadraticForm.tmul, ← e1, BilinForm.tmul]
   dsimp
   have : Subsingleton (Invertible (2 : A)) := inferInstance
   convert associated_left_inverse A ((associated_isSymm A Q₁).tmul (associated_isSymm R Q₂))
 
 theorem polarBilin_tmul [Invertible (2 : A)] (Q₁ : QuadraticForm A M₁) (Q₂ : QuadraticForm R M₂) :
-    polarBilin (Q₁.tmul Q₂) = ⅟(2 : A) • (polarBilin Q₁).tmul (polarBilin Q₂) := by
-  simp_rw [← two_nsmul_associated A, ← two_nsmul_associated R, BilinMap.tmul, tmul_smul,
+    polarBilin (Q₁.tmul Q₂) = ⅟(2 : A) • BilinForm.tmul (polarBilin Q₁) (polarBilin Q₂) := by
+  simp_rw [← two_nsmul_associated A, ← two_nsmul_associated R, BilinForm.tmul, tmul_smul,
     ← smul_tmul', map_nsmul, associated_tmul]
   rw [smul_comm (_ : A) (_ : ℕ), ← smul_assoc, two_smul _ (_ : A), invOf_two_add_invOf_two,
     one_smul]
@@ -95,17 +136,19 @@ theorem baseChange_tmul (Q : QuadraticForm R M₂) (a : A) (m₂ : M₂) :
   tensorDistrib_tmul _ _ _ _
 
 theorem associated_baseChange [Invertible (2 : A)] (Q : QuadraticForm R M₂) :
-    associated (R := A) (Q.baseChange A) = (associated (R := R) Q).baseChange A := by
+    associated (R := A) (Q.baseChange A) = BilinForm.baseChange A (associated (R := R) Q) := by
   dsimp only [QuadraticForm.baseChange, LinearMap.baseChange]
   rw [associated_tmul (QuadraticMap.sq (R := A)) Q, associated_sq]
   exact rfl
 
 theorem polarBilin_baseChange [Invertible (2 : A)] (Q : QuadraticForm R M₂) :
-    polarBilin (Q.baseChange A) = (polarBilin Q).baseChange A := by
-  rw [QuadraticForm.baseChange, BilinMap.baseChange, polarBilin_tmul, BilinMap.tmul,
+    polarBilin (Q.baseChange A) = BilinForm.baseChange A (polarBilin Q) := by
+  rw [QuadraticForm.baseChange, BilinForm.baseChange, polarBilin_tmul, BilinForm.tmul,
     ← LinearMap.map_smul, smul_tmul', ← two_nsmul_associated R, coe_associatedHom, associated_sq,
     smul_comm, ← smul_assoc, two_smul, invOf_two_add_invOf_two, one_smul]
 
+end QuadraticForm
+
 end InvertibleTwo
 
 /-- If two quadratic forms from `A ⊗[R] M₂` agree on elements of the form `1 ⊗ m`, they are equal.
@@ -133,5 +176,3 @@ theorem baseChange_ext ⦃Q₁ Q₂ : QuadraticForm A (A ⊗[R] M₂)⦄
     linear_combination this + hx + hy
 
 end CommRing
-
-end QuadraticForm