refactor(LinearAlgebra/QuadraticForm): Replace BilinForm with a sca…

…lar valued bi `LinearMap` (#10238)

Following on from #10097, which converted the companion of a quadratic form with a bilinear map, this PR replaces a number of results about quadratic forms and bilinear forms with results about quadratic forms and scalar valued bilinear maps. The long term aim is to be able to consider quadratic maps.

The main change is to `LinearAlgebra/QuadraticForm/Basic`, but this necessitates changes throughout `LinearAlgebra/QuadraticForm/`. Minor changes are also required elsewhere:

- `LinearAlgebra/CliffordAlgebra/`
- `LinearAlgebra/Matrix/PosDef`
- `LinearAlgebra/SesquilinearForm`
- A number of additional results about tensor products and linear maps are also required.



Co-authored-by: Eric Wieser <wieser.eric@gmail.com>
Co-authored-by: Christopher Hoskin <christopher.hoskin@overleaf.com>

Counterexamples/CliffordAlgebra_not_injective.lean

@@ -38,6 +38,8 @@ noncomputable section
 
 open scoped BigOperators
 
+open LinearMap (BilinForm)
+
 namespace Q60596
 
 open MvPolynomial
@@ -300,6 +302,6 @@ theorem QuadraticForm.not_forall_mem_range_toQuadraticForm.{v} :
   fun h => Q_not_in_range_toQuadraticForm <| by
     let uU := ULift.moduleEquiv (R := K) (M := L)
     obtain ⟨x, hx⟩ := h K (ULift L) (Q.comp uU)
-    refine ⟨x.comp uU.symm uU.symm, ?_⟩
+    refine ⟨x.compl₁₂ uU.symm uU.symm, ?_⟩
     ext
     simp [BilinForm.toQuadraticForm_comp_same, hx]

Counterexamples/QuadraticForm.lean

@@ -10,26 +10,27 @@ import Mathlib.Data.ZMod.Basic
 #align_import quadratic_form from "leanprover-community/mathlib"@"328375597f2c0dd00522d9c2e5a33b6a6128feeb"
 
 /-!
-# `QuadraticForm R M` and `Subtype BilinForm.IsSymm` are distinct notions in characteristic 2
+# `QuadraticForm R M` and `Subtype LinearMap.IsSymm` are distinct notions in characteristic 2
 
-The main result of this file is `BilinForm.not_injOn_toQuadraticForm_isSymm`.
+The main result of this file is `LinearMap.BilinForm.not_injOn_toQuadraticForm_isSymm`.
 
 The counterexample we use is $B (x, y) (x', y') ↦ xy' + x'y$ where `x y x' y' : ZMod 2`.
 -/
 
 
 variable (F : Type*) [Nontrivial F] [CommRing F] [CharP F 2]
 
-open BilinForm
+open LinearMap
+open LinearMap.BilinForm
+open LinearMap (BilinForm)
 
 namespace Counterexample
 
 set_option linter.uppercaseLean3 false
 
 /-- The bilinear form we will use as a counterexample, over some field `F` of characteristic two. -/
 def B : BilinForm F (F × F) :=
-  BilinForm.linMulLin (LinearMap.fst _ _ _) (LinearMap.snd _ _ _) +
-    BilinForm.linMulLin (LinearMap.snd _ _ _) (LinearMap.fst _ _ _)
+  (mul F F).compl₁₂ (fst _ _ _) (snd _ _ _) + (mul F F).compl₁₂ (snd _ _ _) (fst _ _ _)
 #align counterexample.B Counterexample.B
 
 @[simp]
@@ -43,22 +44,22 @@ theorem isSymm_B : (B F).IsSymm := fun x y => by simp [mul_comm, add_comm]
 theorem isAlt_B : (B F).IsAlt := fun x => by simp [mul_comm, CharTwo.add_self_eq_zero (x.1 * x.2)]
 #align counterexample.is_alt_B Counterexample.isAlt_B
 
-theorem B_ne_zero : B F ≠ 0 := fun h => by simpa using BilinForm.congr_fun h (1, 0) (1, 1)
+theorem B_ne_zero : B F ≠ 0 := fun h => by simpa using LinearMap.congr_fun₂ h (1, 0) (1, 1)
 #align counterexample.B_ne_zero Counterexample.B_ne_zero
 
-/-- `BilinForm.toQuadraticForm` is not injective on symmetric bilinear forms.
+/-- `LinearMap.BilinForm.toQuadraticForm` is not injective on symmetric bilinear forms.
 
 This disproves a weaker version of `QuadraticForm.associated_left_inverse`.
 -/
-theorem BilinForm.not_injOn_toQuadraticForm_isSymm.{u} :
+theorem LinearMap.BilinForm.not_injOn_toQuadraticForm_isSymm.{u} :
     ¬∀ {R M : Type u} [CommSemiring R] [AddCommMonoid M], ∀ [Module R M],
       Set.InjOn (toQuadraticForm : BilinForm R M → QuadraticForm R M) {B | B.IsSymm} := by
   intro h
   let F := ULift.{u} (ZMod 2)
   apply B_ne_zero F
   apply h (isSymm_B F) isSymm_zero
-  rw [BilinForm.toQuadraticForm_zero, BilinForm.toQuadraticForm_eq_zero]
+  rw [toQuadraticForm_zero, toQuadraticForm_eq_zero]
   exact isAlt_B F
-#align counterexample.bilin_form.not_inj_on_to_quadratic_form_is_symm Counterexample.BilinForm.not_injOn_toQuadraticForm_isSymm
+#align counterexample.bilin_form.not_inj_on_to_quadratic_form_is_symm Counterexample.LinearMap.BilinForm.not_injOn_toQuadraticForm_isSymm
 
 end Counterexample

Mathlib/LinearAlgebra/BilinearForm/TensorProduct.lean

@@ -3,8 +3,7 @@ Copyright (c) 2023 Eric Wieser. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Eric Wieser
 -/
-import Mathlib.LinearAlgebra.BilinearForm.Properties
-import Mathlib.LinearAlgebra.TensorProduct
+import Mathlib.LinearAlgebra.Dual
 import Mathlib.LinearAlgebra.TensorProduct.Tower
 
 #align_import linear_algebra.bilinear_form.tensor_product from "leanprover-community/mathlib"@"f0c8bf9245297a541f468be517f1bde6195105e9"
@@ -14,10 +13,10 @@ import Mathlib.LinearAlgebra.TensorProduct.Tower
 
 ## Main definitions
 
-* `BilinForm.tensorDistrib (B₁ ⊗ₜ B₂)`: the bilinear form on `M₁ ⊗ M₂` constructed by applying
-  `B₁` on `M₁` and `B₂` on `M₂`.
-* `BilinForm.tensorDistribEquiv`: `BilinForm.tensorDistrib` as an equivalence on finite free
-  modules.
+* `LinearMap.BilinForm.tensorDistrib (B₁ ⊗ₜ B₂)`: the bilinear form on `M₁ ⊗ M₂` constructed by
+  applying `B₁` on `M₁` and `B₂` on `M₂`.
+* `LinearMap.BilinForm.tensorDistribEquiv`: `BilinForm.tensorDistrib` as an equivalence on finite
+  free modules.
 
 -/
 
@@ -29,8 +28,12 @@ variable {ι : Type uι} {R : Type uR} {A : Type uA} {M₁ : Type uM₁} {M₂ :
 
 open TensorProduct
 
+namespace LinearMap
+
 namespace BilinForm
 
+open LinearMap (BilinForm)
+
 section CommSemiring
 variable [CommSemiring R] [CommSemiring A]
 variable [AddCommMonoid M₁] [AddCommMonoid M₂]
@@ -45,13 +48,12 @@ Note this is heterobasic; the bilinear form on the left can take values in an (c
 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
-    ≪≫ₗ LinearMap.toBilin).toLinearMap
+    ≪≫ₗ (TensorProduct.lift.equiv A (M₁ ⊗[R] M₂) (M₁ ⊗[R] M₂) A).symm).toLinearMap
   ∘ₗ TensorProduct.AlgebraTensorModule.dualDistrib R _ _ _
   ∘ₗ (TensorProduct.AlgebraTensorModule.congr
-    (BilinForm.toLin ≪≫ₗ TensorProduct.lift.equiv A _ _ _)
-    (BilinForm.toLin ≪≫ₗ TensorProduct.lift.equiv R _ _ _)).toLinearMap
-#align bilin_form.tensor_distrib BilinForm.tensorDistrib
+    (TensorProduct.lift.equiv A M₁ M₁ A)
+    (TensorProduct.lift.equiv R _ _ _)).toLinearMap
+#align bilin_form.tensor_distrib LinearMap.BilinForm.tensorDistrib
 
 -- 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.
@@ -61,27 +63,26 @@ theorem tensorDistrib_tmul (B₁ : BilinForm A M₁) (B₂ : BilinForm R M₂) (
     tensorDistrib R A (B₁ ⊗ₜ B₂) (m₁ ⊗ₜ m₂) (m₁' ⊗ₜ m₂')
       = B₂ m₂ m₂' • B₁ m₁ m₁' :=
   rfl
-#align bilin_form.tensor_distrib_tmul BilinForm.tensorDistrib_tmulₓ
+#align bilin_form.tensor_distrib_tmul LinearMap.BilinForm.tensorDistrib_tmulₓ
 
 /-- The tensor product of two bilinear forms, a shorthand for dot notation. -/
 @[reducible]
 protected def tmul (B₁ : BilinForm A M₁) (B₂ : BilinForm R M₂) : BilinForm A (M₁ ⊗[R] M₂) :=
   tensorDistrib R A (B₁ ⊗ₜ[R] B₂)
-#align bilin_form.tmul BilinForm.tmul
+#align bilin_form.tmul LinearMap.BilinForm.tmul
 
 attribute [ext] TensorProduct.ext in
 /-- A tensor product of symmetric bilinear forms is symmetric. -/
-lemma IsSymm.tmul {B₁ : BilinForm A M₁} {B₂ : BilinForm R M₂}
+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 [isSymm_iff_flip R]
-  apply toLin.injective
+  rw [LinearMap.isSymm_iff_eq_flip]
   ext x₁ x₂ y₁ y₂
-  exact (congr_arg₂ (HSMul.hSMul) (hB₂ x₂ y₂) (hB₁ x₁ y₁)).symm
+  exact congr_arg₂ (HSMul.hSMul) (hB₂ x₂ y₂) (hB₁ x₁ y₁)
 
 variable (A) in
 /-- The base change of a bilinear form. -/
 protected def baseChange (B : BilinForm R M₂) : BilinForm A (A ⊗[R] M₂) :=
-  BilinForm.tmul (R := R) (A := A) (M₁ := A) (M₂ := M₂) (LinearMap.toBilin <| LinearMap.mul A A) B
+  BilinForm.tmul (R := R) (A := A) (M₁ := A) (M₂ := M₂) (LinearMap.mul A A) B
 
 @[simp]
 theorem baseChange_tmul (B₂ : BilinForm R M₂) (a : A) (m₂ : M₂)
@@ -116,12 +117,11 @@ noncomputable def tensorDistribEquiv :
     BilinForm R M₁ ⊗[R] BilinForm R M₂ ≃ₗ[R] BilinForm R (M₁ ⊗[R] M₂) :=
   -- the same `LinearEquiv`s as from `tensorDistrib`,
   -- but with the inner linear map also as an equiv
-  TensorProduct.congr (BilinForm.toLin ≪≫ₗ TensorProduct.lift.equiv R _ _ _)
-    (BilinForm.toLin ≪≫ₗ TensorProduct.lift.equiv R _ _ _) ≪≫ₗ
+  TensorProduct.congr (TensorProduct.lift.equiv R _ _ _) (TensorProduct.lift.equiv R _ _ _) ≪≫ₗ
   TensorProduct.dualDistribEquiv R (M₁ ⊗ M₁) (M₂ ⊗ M₂) ≪≫ₗ
   (TensorProduct.tensorTensorTensorComm R _ _ _ _).dualMap ≪≫ₗ
-  (TensorProduct.lift.equiv R _ _ _).symm ≪≫ₗ LinearMap.toBilin
-#align bilin_form.tensor_distrib_equiv BilinForm.tensorDistribEquiv
+  (TensorProduct.lift.equiv R _ _ _).symm
+#align bilin_form.tensor_distrib_equiv LinearMap.BilinForm.tensorDistribEquiv
 
 -- this is a dsimp lemma
 @[simp, nolint simpNF]
@@ -137,16 +137,17 @@ variable (R M₁ M₂) in
 theorem tensorDistribEquiv_toLinearMap :
     (tensorDistribEquiv R (M₁ := M₁) (M₂ := M₂)).toLinearMap = tensorDistrib R R := by
   ext B₁ B₂ : 3
-  apply toLin.injective
   ext
   exact mul_comm _ _
 
 @[simp]
 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
-#align bilin_form.tensor_distrib_equiv_apply BilinForm.tensorDistribEquiv_apply
+#align bilin_form.tensor_distrib_equiv_apply LinearMap.BilinForm.tensorDistribEquiv_apply
 
 end CommRing
 
 end BilinForm
+
+end LinearMap

Mathlib/LinearAlgebra/CliffordAlgebra/BaseChange.lean

@@ -94,8 +94,8 @@ 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, BilinForm.baseChange_tmul, one_mul,
-      TensorProduct.smul_tmul, Algebra.algebraMap_eq_smul_one, QuadraticForm.polarBilin_apply]
+      QuadraticForm.polarBilin_baseChange, LinearMap.BilinForm.baseChange_tmul, one_mul,
+      TensorProduct.smul_tmul, Algebra.algebraMap_eq_smul_one, QuadraticForm.polarBilin_apply_apply]
 
 @[simp] theorem toBaseChange_ι (Q : QuadraticForm R V) (z : A) (v : V) :
     toBaseChange A Q (ι (Q.baseChange A) (z ⊗ₜ v)) = z ⊗ₜ ι Q v :=

Mathlib/LinearAlgebra/CliffordAlgebra/Basic.lean

@@ -251,7 +251,7 @@ theorem forall_mul_self_eq_iff {A : Type*} [Ring A] [Algebra R A] (h2 : IsUnit (
     (f : M →ₗ[R] A) :
     (∀ x, f x * f x = algebraMap _ _ (Q x)) ↔
       (LinearMap.mul R A).compl₂ f ∘ₗ f + (LinearMap.mul R A).flip.compl₂ f ∘ₗ f =
-        Q.polarBilin.toLin.compr₂ (Algebra.linearMap R A) := by
+        Q.polarBilin.compr₂ (Algebra.linearMap R A) := by
   simp_rw [DFunLike.ext_iff]
   refine ⟨mul_add_swap_eq_polar_of_forall_mul_self_eq _, fun h x => ?_⟩
   change ∀ x y : M, f x * f y + f y * f x = algebraMap R A (QuadraticForm.polar Q x y) at h

Mathlib/LinearAlgebra/CliffordAlgebra/Contraction.lean

@@ -6,6 +6,7 @@ Authors: Eric Wieser
 import Mathlib.LinearAlgebra.ExteriorAlgebra.Basic
 import Mathlib.LinearAlgebra.CliffordAlgebra.Fold
 import Mathlib.LinearAlgebra.CliffordAlgebra.Conjugation
+import Mathlib.LinearAlgebra.Dual
 
 #align_import linear_algebra.clifford_algebra.contraction from "leanprover-community/mathlib"@"70fd9563a21e7b963887c9360bd29b2393e6225a"
 
@@ -41,6 +42,7 @@ Within this file, we use the local notation
 
 -/
 
+open LinearMap (BilinForm)
 
 universe u1 u2 u3
 
@@ -243,15 +245,14 @@ local infixl:70 "⌊" => contractRight
 @[simps!]
 def changeFormAux (B : BilinForm R M) : M →ₗ[R] CliffordAlgebra Q →ₗ[R] CliffordAlgebra Q :=
   haveI v_mul := (Algebra.lmul R (CliffordAlgebra Q)).toLinearMap ∘ₗ ι Q
-  v_mul - contractLeft ∘ₗ (BilinForm.toLin B)
+  v_mul - contractLeft ∘ₗ B
 #align clifford_algebra.change_form_aux CliffordAlgebra.changeFormAux
 
 theorem changeFormAux_changeFormAux (B : BilinForm R M) (v : M) (x : CliffordAlgebra Q) :
     changeFormAux Q B v (changeFormAux Q B v x) = (Q v - B v v) • x := by
   simp only [changeFormAux_apply_apply]
   rw [mul_sub, ← mul_assoc, ι_sq_scalar, map_sub, contractLeft_ι_mul, ← sub_add, sub_sub_sub_comm,
-    ← Algebra.smul_def, BilinForm.toLin_apply, sub_self, sub_zero, contractLeft_contractLeft,
-    add_zero, sub_smul]
+    ← Algebra.smul_def, sub_self, sub_zero, contractLeft_contractLeft, add_zero, sub_smul]
 #align clifford_algebra.change_form_aux_change_form_aux CliffordAlgebra.changeFormAux_changeFormAux
 
 variable {Q}
@@ -311,15 +312,15 @@ theorem changeForm_ι (m : M) : changeForm h (ι (M := M) Q m) = ι (M := M) Q'
 
 theorem changeForm_ι_mul (m : M) (x : CliffordAlgebra Q) :
     changeForm h (ι (M := M) Q m * x) = ι (M := M) Q' m * changeForm h x
-    - contractLeft (Q := Q') (BilinForm.toLin B m) (changeForm h x) :=
+    - contractLeft (Q := Q') (B m) (changeForm h x) :=
 -- Porting note: original statement
 --    - BilinForm.toLin B m⌋changeForm h x :=
   (foldr_mul _ _ _ _ _ _).trans <| by rw [foldr_ι]; rfl
 #align clifford_algebra.change_form_ι_mul CliffordAlgebra.changeForm_ι_mul
 
 theorem changeForm_ι_mul_ι (m₁ m₂ : M) :
     changeForm h (ι Q m₁ * ι Q m₂) = ι Q' m₁ * ι Q' m₂ - algebraMap _ _ (B m₁ m₂) := by
-  rw [changeForm_ι_mul, changeForm_ι, contractLeft_ι, BilinForm.toLin_apply]
+  rw [changeForm_ι_mul, changeForm_ι, contractLeft_ι]
 #align clifford_algebra.change_form_ι_mul_ι CliffordAlgebra.changeForm_ι_mul_ι
 
 /-- Theorem 23 of [grinberg_clifford_2016][] -/
@@ -339,7 +340,7 @@ theorem changeForm_self_apply (x : CliffordAlgebra Q) : changeForm (Q' := Q)
   induction' x using CliffordAlgebra.left_induction with r x y hx hy m x hx
   · simp_rw [changeForm_algebraMap]
   · rw [map_add, hx, hy]
-  · rw [changeForm_ι_mul, hx, map_zero, LinearMap.zero_apply, map_zero, LinearMap.zero_apply,
+  · rw [changeForm_ι_mul, hx, LinearMap.zero_apply, map_zero, LinearMap.zero_apply,
       sub_zero]
 #align clifford_algebra.change_form_self_apply CliffordAlgebra.changeForm_self_apply
 
@@ -355,7 +356,7 @@ theorem changeForm_changeForm (x : CliffordAlgebra Q) :
   induction' x using CliffordAlgebra.left_induction with r x y hx hy m x hx
   · simp_rw [changeForm_algebraMap]
   · rw [map_add, map_add, map_add, hx, hy]
-  · rw [changeForm_ι_mul, map_sub, changeForm_ι_mul, changeForm_ι_mul, hx, sub_sub, map_add,
+  · rw [changeForm_ι_mul, map_sub, changeForm_ι_mul, changeForm_ι_mul, hx, sub_sub,
       LinearMap.add_apply, map_add, LinearMap.add_apply, changeForm_contractLeft, hx,
       add_comm (_ : CliffordAlgebra Q'')]
 #align clifford_algebra.change_form_change_form CliffordAlgebra.changeForm_changeForm
@@ -375,11 +376,12 @@ def changeFormEquiv : CliffordAlgebra Q ≃ₗ[R] CliffordAlgebra Q' :=
     invFun := changeForm (changeForm.neg_proof h)
     left_inv := fun x => by
       dsimp only
-      exact (changeForm_changeForm _ _ x).trans <| by simp_rw [add_right_neg, changeForm_self_apply]
+      exact (changeForm_changeForm _ _ x).trans <|
+        by simp_rw [(add_neg_self B), changeForm_self_apply]
     right_inv := fun x => by
       dsimp only
       exact (changeForm_changeForm _ _ x).trans <|
-        by simp_rw [add_left_neg, changeForm_self_apply] }
+        by simp_rw [(add_left_neg B), changeForm_self_apply] }
 #align clifford_algebra.change_form_equiv CliffordAlgebra.changeFormEquiv
 
 @[simp]

Mathlib/LinearAlgebra/Matrix/PosDef.lean

@@ -325,15 +325,16 @@ theorem transpose {M : Matrix n n R} (hM : M.PosDef) : Mᵀ.PosDef := by
 theorem of_toQuadraticForm' [DecidableEq n] {M : Matrix n n ℝ} (hM : M.IsSymm)
     (hMq : M.toQuadraticForm'.PosDef) : M.PosDef := by
   refine' ⟨hM, fun x hx => _⟩
-  simp only [toQuadraticForm', QuadraticForm.PosDef, BilinForm.toQuadraticForm_apply,
-    Matrix.toBilin'_apply'] at hMq
+  simp only [toQuadraticForm', QuadraticForm.PosDef, LinearMap.BilinForm.toQuadraticForm_apply,
+    toLinearMap₂'_apply'] at hMq
   apply hMq x hx
 #align matrix.pos_def_of_to_quadratic_form' Matrix.PosDef.of_toQuadraticForm'
 
 theorem toQuadraticForm' [DecidableEq n] {M : Matrix n n ℝ} (hM : M.PosDef) :
     M.toQuadraticForm'.PosDef := by
   intro x hx
-  simp only [Matrix.toQuadraticForm', BilinForm.toQuadraticForm_apply, Matrix.toBilin'_apply']
+  simp only [Matrix.toQuadraticForm', LinearMap.BilinForm.toQuadraticForm_apply,
+    toLinearMap₂'_apply']
   apply hM.2 x hx
 #align matrix.pos_def_to_quadratic_form' Matrix.PosDef.toQuadraticForm'
 
@@ -366,14 +367,14 @@ variable {n : Type*} [Fintype n]
 theorem posDef_of_toMatrix' [DecidableEq n] {Q : QuadraticForm ℝ (n → ℝ)}
     (hQ : Q.toMatrix'.PosDef) : Q.PosDef := by
   rw [← toQuadraticForm_associated ℝ Q,
-    ← BilinForm.toMatrix'.left_inv ((associatedHom (R := ℝ) ℝ) Q)]
+    ← LinearMap.toMatrix₂'.left_inv ((associatedHom (R := ℝ) ℝ) Q)]
   exact hQ.toQuadraticForm'
 #align quadratic_form.pos_def_of_to_matrix' QuadraticForm.posDef_of_toMatrix'
 
 theorem posDef_toMatrix' [DecidableEq n] {Q : QuadraticForm ℝ (n → ℝ)} (hQ : Q.PosDef) :
     Q.toMatrix'.PosDef := by
   rw [← toQuadraticForm_associated ℝ Q, ←
-    BilinForm.toMatrix'.left_inv ((associatedHom (R := ℝ) ℝ) Q)] at hQ
+    LinearMap.toMatrix₂'.left_inv ((associatedHom (R := ℝ) ℝ) Q)] at hQ
   exact .of_toQuadraticForm' (isSymm_toMatrix' Q) hQ
 #align quadratic_form.pos_def_to_matrix' QuadraticForm.posDef_toMatrix'