refactor(LinearAlgebra/QuadraticForm/Basic) : Generalise `QuadraticFo…

…rm` to `QuadraticMap` (#7569)

Most of the theory in `LinearAlgebra/QuadraticForm/Basic` also holds for Quadratic Maps with minimal modification. A quadratic form is just a special case of a quadratic map.

To keep this PR to a reasonable size I have not attempted to generalise other files in `LinearAlgebra/QuadraticForm` - this can be done in subsequent PRs.

To facilitate dot notation we also introduce `LinearMap.BilinMap` as an abbreviation for `M →ₗ[R] M →ₗ[R] N`. No attempt has been made to generalise all `BilinForm` results to `BilinMap` at this stage.

Some results in `LinearAlgebra/QuadraticForm/Basic` are still stated for quadratic forms either because there was no obvious generalisation to quadratic maps, or the generalisation requires improvements elsewhere in Mathlib which can be considered in subsequent PRs.

My motivation for introducing Quadratic Maps to Mathlib is that it would allow the definition of interesting non-associative structures such as quadratic Jordan Algebras and Jordan Pairs.



Co-authored-by: Eric Wieser <[email protected]>
Co-authored-by: Christopher Hoskin <[email protected]>
Co-authored-by: Christopher Hoskin <[email protected]>

Counterexamples/CliffordAlgebraNotInjective.lean

@@ -37,6 +37,7 @@ are quadratic forms that cannot be expressed via even non-symmetric bilinear for
 noncomputable section
 
 open LinearMap (BilinForm)
+open LinearMap (BilinMap)
 
 namespace Q60596
 
@@ -149,7 +150,7 @@ abbrev L : Type _ := _ ⧸ LinearMap.ker lFunc
 
 /-- The quadratic form corresponding to squaring a single coefficient. -/
 def sq {ι R : Type*} [CommRing R] (i : ι) : QuadraticForm R (ι → R) :=
-  QuadraticForm.sq.comp <| LinearMap.proj i
+  QuadraticMap.sq.comp <| LinearMap.proj i
 
 theorem sq_map_add_char_two {ι R : Type*} [CommRing R] [CharP R 2] (i : ι) (a b : ι → R) :
     sq i (a + b) = sq i a + sq i b :=
@@ -165,10 +166,10 @@ def Q' : QuadraticForm K (Fin 3 → K) :=
   ∑ i, sq i
 
 theorem Q'_add (x y : Fin 3 → K) : Q' (x + y) = Q' x + Q' y := by
-  simp only [Q', QuadraticForm.sum_apply, sq_map_add_char_two, Finset.sum_add_distrib]
+  simp only [Q', QuadraticMap.sum_apply, sq_map_add_char_two, Finset.sum_add_distrib]
 
 theorem Q'_sub (x y : Fin 3 → K) : Q' (x - y) = Q' x - Q' y := by
-  simp only [Q', QuadraticForm.sum_apply, sq_map_sub_char_two, Finset.sum_sub_distrib]
+  simp only [Q', QuadraticMap.sum_apply, sq_map_sub_char_two, Finset.sum_sub_distrib]
 
 theorem Q'_apply (a : Fin 3 → K) : Q' a = a 0 * a 0 + a 1 * a 1 + a 2 * a 2 :=
   calc
@@ -204,7 +205,7 @@ theorem Q'_zero_under_ideal (v : Fin 3 → K) (hv : v ∈ LinearMap.ker lFunc) :
 /-- `Q'`, lifted to operate on the quotient space `L`. -/
 @[simps!]
 def Q : QuadraticForm K L :=
-  QuadraticForm.ofPolar
+  QuadraticMap.ofPolar
     (fun x =>
       Quotient.liftOn' x Q' fun a b h => by
         rw [Submodule.quotientRel_r_def] at h
@@ -263,7 +264,7 @@ theorem algebraMap_not_injective : ¬Function.Injective (algebraMap K <| Cliffor
   fun h => αβγ_ne_zero <| h <| by rw [algebraMap_αβγ_eq_zero, RingHom.map_zero]
 
 /-- Bonus counterexample: `Q` is a quadratic form that has no bilinear form. -/
-theorem Q_not_in_range_toQuadraticForm : Q ∉ Set.range BilinForm.toQuadraticForm := by
+theorem Q_not_in_range_toQuadraticForm : Q ∉ Set.range BilinMap.toQuadraticMap := by
   rintro ⟨B, hB⟩
   rw [← sub_zero Q] at hB
   apply algebraMap_not_injective
@@ -294,10 +295,10 @@ open Q60596 in
 theorem QuadraticForm.not_forall_mem_range_toQuadraticForm.{v} :
     -- TODO: make `R` universe polymorphic
     ¬∀ (R : Type) (M : Type v) [CommRing R] [AddCommGroup M] [Module R M] (Q : QuadraticForm R M),
-      Q ∈ Set.range BilinForm.toQuadraticForm :=
+      Q ∈ Set.range BilinMap.toQuadraticMap :=
   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.compl₁₂ uU.symm uU.symm, ?_⟩
     ext
-    simp [BilinForm.toQuadraticForm_comp_same, hx]
+    simp [BilinMap.toQuadraticMap_comp_same, hx]

Counterexamples/QuadraticForm.lean

@@ -23,6 +23,7 @@ variable (F : Type*) [Nontrivial F] [CommRing F] [CharP F 2]
 open LinearMap
 open LinearMap.BilinForm
 open LinearMap (BilinForm)
+open LinearMap.BilinMap
 
 namespace Counterexample
 
@@ -53,12 +54,12 @@ This disproves a weaker version of `QuadraticForm.associated_left_inverse`.
 -/
 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
+      Set.InjOn (toQuadraticMap : 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 [toQuadraticForm_zero, toQuadraticForm_eq_zero]
+  rw [toQuadraticMap_zero, toQuadraticMap_eq_zero]
   exact isAlt_B F
 #align counterexample.bilin_form.not_inj_on_to_quadratic_form_is_symm Counterexample.LinearMap.BilinForm.not_injOn_toQuadraticForm_isSymm
 

Mathlib/LinearAlgebra/BilinearForm/TensorProduct.lean

@@ -13,9 +13,9 @@ import Mathlib.LinearAlgebra.TensorProduct.Tower
 
 ## Main definitions
 
-* `LinearMap.BilinForm.tensorDistrib (B₁ ⊗ₜ B₂)`: the bilinear form on `M₁ ⊗ M₂` constructed by
+* `LinearMap.BilinMap.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
+* `LinearMap.BilinMap.tensorDistribEquiv`: `BilinForm.tensorDistrib` as an equivalence on finite
   free modules.
 
 -/
@@ -30,8 +30,9 @@ open TensorProduct
 
 namespace LinearMap
 
-namespace BilinForm
+namespace BilinMap
 
+open LinearMap (BilinMap)
 open LinearMap (BilinForm)
 
 section CommSemiring
@@ -53,7 +54,7 @@ def tensorDistrib : BilinForm A M₁ ⊗[R] BilinForm R M₂ →ₗ[A] BilinForm
   ∘ₗ (TensorProduct.AlgebraTensorModule.congr
     (TensorProduct.lift.equiv A M₁ M₁ A)
     (TensorProduct.lift.equiv R _ _ _)).toLinearMap
-#align bilin_form.tensor_distrib LinearMap.BilinForm.tensorDistrib
+#align bilin_form.tensor_distrib LinearMap.BilinMap.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.
@@ -63,28 +64,28 @@ 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 LinearMap.BilinForm.tensorDistrib_tmulₓ
+#align bilin_form.tensor_distrib_tmul LinearMap.BilinMap.tensorDistrib_tmulₓ
 
 /-- The tensor product of two bilinear forms, a shorthand for dot notation. -/
-protected abbrev tmul (B₁ : BilinForm A M₁) (B₂ : BilinForm R M₂) : BilinForm A (M₁ ⊗[R] M₂) :=
+protected abbrev tmul (B₁ : BilinMap A M₁ A) (B₂ : BilinMap  R M₂ R) : BilinMap A (M₁ ⊗[R] M₂) A :=
   tensorDistrib R A (B₁ ⊗ₜ[R] B₂)
-#align bilin_form.tmul LinearMap.BilinForm.tmul
+#align bilin_form.tmul LinearMap.BilinMap.tmul
 
 attribute [local ext] TensorProduct.ext in
 /-- A tensor product of symmetric bilinear forms is symmetric. -/
-lemma _root_.LinearMap.IsSymm.tmul {B₁ : BilinForm A M₁} {B₂ : BilinForm R M₂}
+lemma _root_.LinearMap.IsSymm.tmul {B₁ : BilinMap A M₁ A} {B₂ : BilinMap R M₂ R}
     (hB₁ : B₁.IsSymm) (hB₂ : B₂.IsSymm) : (B₁.tmul B₂).IsSymm := by
   rw [LinearMap.isSymm_iff_eq_flip]
   ext x₁ x₂ y₁ y₂
   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.mul A A) B
+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
 
 @[simp]
-theorem baseChange_tmul (B₂ : BilinForm R M₂) (a : A) (m₂ : M₂)
+theorem baseChange_tmul (B₂ : BilinMap R M₂ R) (a : A) (m₂ : M₂)
     (a' : A) (m₂' : M₂) :
     B₂.baseChange A (a ⊗ₜ m₂) (a' ⊗ₜ m₂') = (B₂ m₂ m₂') • (a * a') :=
   rfl
@@ -115,7 +116,7 @@ noncomputable def tensorDistribEquiv :
   TensorProduct.dualDistribEquiv R (M₁ ⊗ M₁) (M₂ ⊗ M₂) ≪≫ₗ
   (TensorProduct.tensorTensorTensorComm R _ _ _ _).dualMap ≪≫ₗ
   (TensorProduct.lift.equiv R _ _ _).symm
-#align bilin_form.tensor_distrib_equiv LinearMap.BilinForm.tensorDistribEquiv
+#align bilin_form.tensor_distrib_equiv LinearMap.BilinMap.tensorDistribEquiv
 
 @[simp]
 theorem tensorDistribEquiv_tmul (B₁ : BilinForm R M₁) (B₂ : BilinForm R M₂) (m₁ : M₁) (m₂ : M₂)
@@ -137,10 +138,10 @@ theorem tensorDistribEquiv_toLinearMap :
 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 LinearMap.BilinForm.tensorDistribEquiv_apply
+#align bilin_form.tensor_distrib_equiv_apply LinearMap.BilinMap.tensorDistribEquiv_apply
 
 end CommRing
 
-end BilinForm
+end BilinMap
 
 end LinearMap

Mathlib/LinearAlgebra/BilinearMap.lean

@@ -393,9 +393,6 @@ theorem compr₂_apply (f : M →ₗ[R] Nₗ →ₗ[R] Pₗ) (g : Pₗ →ₗ[R]
 
 variable (R M)
 
-/-- For convenience, a shorthand for the type of bilinear forms from `M` to `R`. -/
-protected abbrev BilinForm : Type _ := M →ₗ[R] M →ₗ[R] R
-
 /-- Scalar multiplication as a bilinear map `R → M → M`. -/
 def lsmul : R →ₗ[R] M →ₗ[R] M :=
   mk₂ R (· • ·) add_smul (fun _ _ _ => mul_smul _ _ _) smul_add fun r s m => by
@@ -413,6 +410,14 @@ variable {M}
 theorem lsmul_apply (r : R) (m : M) : lsmul R M r m = r • m := rfl
 #align linear_map.lsmul_apply LinearMap.lsmul_apply
 
+variable (R M Nₗ) in
+/-- A shorthand for the type of `R`-bilinear `Nₗ`-valued maps on `M`. -/
+protected abbrev BilinMap : Type _ := M →ₗ[R] M →ₗ[R] Nₗ
+
+variable (R M) in
+/-- For convenience, a shorthand for the type of bilinear forms from `M` to `R`. -/
+protected abbrev BilinForm : Type _ := LinearMap.BilinMap R M R
+
 end CommSemiring
 
 section CommRing

Mathlib/LinearAlgebra/CliffordAlgebra/BaseChange.lean

@@ -85,7 +85,7 @@ noncomputable def toBaseChange (Q : QuadraticForm R V) :
     letI : Invertible (2 : A ⊗[R] CliffordAlgebra Q) :=
       (Invertible.map (algebraMap R _) 2).copy 2 (map_ofNat _ _).symm
     suffices hpure_tensor : ∀ v w, (1 * 1) ⊗ₜ[R] (ι Q v * ι Q w) + (1 * 1) ⊗ₜ[R] (ι Q w * ι Q v) =
-        QuadraticForm.polarBilin (Q.baseChange A) (1 ⊗ₜ[R] v) (1 ⊗ₜ[R] w) ⊗ₜ[R] 1 by
+        QuadraticMap.polarBilin (Q.baseChange A) (1 ⊗ₜ[R] v) (1 ⊗ₜ[R] w) ⊗ₜ[R] 1 by
       -- the crux is that by converting to a statement about linear maps instead of quadratic forms,
       -- we then have access to all the partially-applied `ext` lemmas.
       rw [CliffordAlgebra.forall_mul_self_eq_iff (isUnit_of_invertible _)]
@@ -95,8 +95,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, LinearMap.BilinForm.baseChange_tmul, one_mul,
-      TensorProduct.smul_tmul, Algebra.algebraMap_eq_smul_one, QuadraticForm.polarBilin_apply_apply]
+      QuadraticForm.polarBilin_baseChange, LinearMap.BilinMap.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) :
     toBaseChange A Q (ι (Q.baseChange A) (z ⊗ₜ v)) = z ⊗ₜ ι Q v :=

Mathlib/LinearAlgebra/CliffordAlgebra/Basic.lean

@@ -235,14 +235,14 @@ theorem induction {C : CliffordAlgebra Q → Prop}
 
 theorem mul_add_swap_eq_polar_of_forall_mul_self_eq {A : Type*} [Ring A] [Algebra R A]
     (f : M →ₗ[R] A) (hf : ∀ x, f x * f x = algebraMap _ _ (Q x)) (a b : M) :
-    f a * f b + f b * f a = algebraMap R _ (QuadraticForm.polar Q a b) :=
+    f a * f b + f b * f a = algebraMap R _ (QuadraticMap.polar Q a b) :=
   calc
     f a * f b + f b * f a = f (a + b) * f (a + b) - f a * f a - f b * f b := by
       rw [f.map_add, mul_add, add_mul, add_mul]; abel
     _ = algebraMap R _ (Q (a + b)) - algebraMap R _ (Q a) - algebraMap R _ (Q b) := by
       rw [hf, hf, hf]
     _ = algebraMap R _ (Q (a + b) - Q a - Q b) := by rw [← RingHom.map_sub, ← RingHom.map_sub]
-    _ = algebraMap R _ (QuadraticForm.polar Q a b) := rfl
+    _ = algebraMap R _ (QuadraticMap.polar Q a b) := rfl
 
 /-- An alternative way to provide the argument to `CliffordAlgebra.lift` when `2` is invertible.
 
@@ -255,18 +255,18 @@ theorem forall_mul_self_eq_iff {A : Type*} [Ring A] [Algebra R A] (h2 : IsUnit (
         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
+  change ∀ x y : M, f x * f y + f y * f x = algebraMap R A (QuadraticMap.polar Q x y) at h
   apply h2.mul_left_cancel
-  rw [two_mul, two_mul, h x x, QuadraticForm.polar_self, two_mul, map_add]
+  rw [two_mul, two_mul, h x x, QuadraticMap.polar_self, two_smul, map_add]
 
 /-- The symmetric product of vectors is a scalar -/
 theorem ι_mul_ι_add_swap (a b : M) :
-    ι Q a * ι Q b + ι Q b * ι Q a = algebraMap R _ (QuadraticForm.polar Q a b) :=
+    ι Q a * ι Q b + ι Q b * ι Q a = algebraMap R _ (QuadraticMap.polar Q a b) :=
   mul_add_swap_eq_polar_of_forall_mul_self_eq _ (ι_sq_scalar _) _ _
 #align clifford_algebra.ι_mul_ι_add_swap CliffordAlgebra.ι_mul_ι_add_swap
 
 theorem ι_mul_ι_comm (a b : M) :
-    ι Q a * ι Q b = algebraMap R _ (QuadraticForm.polar Q a b) - ι Q b * ι Q a :=
+    ι Q a * ι Q b = algebraMap R _ (QuadraticMap.polar Q a b) - ι Q b * ι Q a :=
   eq_sub_of_add_eq (ι_mul_ι_add_swap a b)
 #align clifford_algebra.ι_mul_comm CliffordAlgebra.ι_mul_ι_comm
 
@@ -293,7 +293,7 @@ end isOrtho
 
 /-- $aba$ is a vector. -/
 theorem ι_mul_ι_mul_ι (a b : M) :
-    ι Q a * ι Q b * ι Q a = ι Q (QuadraticForm.polar Q a b • a - Q a • b) := by
+    ι Q a * ι Q b * ι Q a = ι Q (QuadraticMap.polar Q a b • a - Q a • b) := by
   rw [ι_mul_ι_comm, sub_mul, mul_assoc, ι_sq_scalar, ← Algebra.smul_def, ← Algebra.commutes, ←
     Algebra.smul_def, ← map_smul, ← map_smul, ← map_sub]
 #align clifford_algebra.ι_mul_ι_mul_ι CliffordAlgebra.ι_mul_ι_mul_ι

Mathlib/LinearAlgebra/CliffordAlgebra/Contraction.lean

@@ -42,6 +42,7 @@ Within this file, we use the local notation
 
 -/
 
+open LinearMap (BilinMap)
 open LinearMap (BilinForm)
 
 universe u1 u2 u3
@@ -255,39 +256,39 @@ theorem changeFormAux_changeFormAux (B : BilinForm R M) (v : M) (x : CliffordAlg
 
 variable {Q}
 variable {Q' Q'' : QuadraticForm R M} {B B' : BilinForm R M}
-variable (h : B.toQuadraticForm = Q' - Q) (h' : B'.toQuadraticForm = Q'' - Q')
+variable (h : B.toQuadraticMap = Q' - Q) (h' : B'.toQuadraticMap = Q'' - Q')
 
 /-- Convert between two algebras of different quadratic form, sending vector to vectors, scalars to
 scalars, and adjusting products by a contraction term.
 
 This is $\lambda_B$ from [bourbaki2007][] $9 Lemma 2. -/
-def changeForm (h : B.toQuadraticForm = Q' - Q) : CliffordAlgebra Q →ₗ[R] CliffordAlgebra Q' :=
+def changeForm (h : B.toQuadraticMap = Q' - Q) : CliffordAlgebra Q →ₗ[R] CliffordAlgebra Q' :=
   foldr Q (changeFormAux Q' B)
     (fun m x =>
       (changeFormAux_changeFormAux Q' B m x).trans <| by
-        dsimp only [← BilinForm.toQuadraticForm_apply]
-        rw [h, QuadraticForm.sub_apply, sub_sub_cancel])
+        dsimp only [← BilinMap.toQuadraticMap_apply]
+        rw [h, QuadraticMap.sub_apply, sub_sub_cancel])
     1
 #align clifford_algebra.change_form CliffordAlgebra.changeForm
 
 /-- Auxiliary lemma used as an argument to `CliffordAlgebra.changeForm` -/
-theorem changeForm.zero_proof : (0 : BilinForm R M).toQuadraticForm = Q - Q :=
+theorem changeForm.zero_proof : (0 : BilinForm R M).toQuadraticMap = Q - Q :=
   (sub_self _).symm
 #align clifford_algebra.change_form.zero_proof CliffordAlgebra.changeForm.zero_proof
 
 /-- Auxiliary lemma used as an argument to `CliffordAlgebra.changeForm` -/
-theorem changeForm.add_proof : (B + B').toQuadraticForm = Q'' - Q :=
+theorem changeForm.add_proof : (B + B').toQuadraticMap = Q'' - Q :=
   (congr_arg₂ (· + ·) h h').trans <| sub_add_sub_cancel' _ _ _
 #align clifford_algebra.change_form.add_proof CliffordAlgebra.changeForm.add_proof
 
 /-- Auxiliary lemma used as an argument to `CliffordAlgebra.changeForm` -/
-theorem changeForm.neg_proof : (-B).toQuadraticForm = Q - Q' :=
+theorem changeForm.neg_proof : (-B).toQuadraticMap = Q - Q' :=
   (congr_arg Neg.neg h).trans <| neg_sub _ _
 #align clifford_algebra.change_form.neg_proof CliffordAlgebra.changeForm.neg_proof
 
 theorem changeForm.associated_neg_proof [Invertible (2 : R)] :
-    (QuadraticForm.associated (R := R) (M := M) (-Q)).toQuadraticForm = 0 - Q := by
-  simp [QuadraticForm.toQuadraticForm_associated]
+    (QuadraticMap.associated (R := R) (M := M) (-Q)).toQuadraticMap = 0 - Q := by
+  simp [QuadraticMap.toQuadraticMap_associated]
 #align clifford_algebra.change_form.associated_neg_proof CliffordAlgebra.changeForm.associated_neg_proof
 
 @[simp]

Mathlib/LinearAlgebra/CliffordAlgebra/Equivs.lean

@@ -127,7 +127,7 @@ open scoped ComplexConjugate
 
 /-- The quadratic form sending elements to the negation of their square. -/
 def Q : QuadraticForm ℝ ℝ :=
-  -QuadraticForm.sq (R := ℝ) -- Porting note: Added `(R := ℝ)`
+  -QuadraticMap.sq (R := ℝ) -- Porting note: Added `(R := ℝ)`
 set_option linter.uppercaseLean3 false in
 #align clifford_algebra_complex.Q CliffordAlgebraComplex.Q
 
@@ -259,7 +259,8 @@ variable {R : Type*} [CommRing R] (c₁ c₂ : R)
 /-- `Q c₁ c₂` is a quadratic form over `R × R` such that `CliffordAlgebra (Q c₁ c₂)` is isomorphic
 as an `R`-algebra to `ℍ[R,c₁,c₂]`. -/
 def Q : QuadraticForm R (R × R) :=
-  (c₁ • QuadraticForm.sq (R := R)).prod (c₂ • QuadraticForm.sq) -- Porting note: Added `(R := R)`
+   -- Porting note: Added `(R := R)`
+  QuadraticForm.prod (c₁ • QuadraticMap.sq (R := R)) (c₂ • QuadraticMap.sq)
 set_option linter.uppercaseLean3 false in
 #align clifford_algebra_quaternion.Q CliffordAlgebraQuaternion.Q
 
@@ -283,7 +284,7 @@ def quaternionBasis : QuaternionAlgebra.Basis (CliffordAlgebra (Q c₁ c₂)) c
     simp
   i_mul_j := rfl
   j_mul_i := by
-    rw [eq_neg_iff_add_eq_zero, ι_mul_ι_add_swap, QuadraticForm.polar]
+    rw [eq_neg_iff_add_eq_zero, ι_mul_ι_add_swap, QuadraticMap.polar]
     simp
 #align clifford_algebra_quaternion.quaternion_basis CliffordAlgebraQuaternion.quaternionBasis
 
@@ -399,7 +400,7 @@ variable {R M : Type*} [CommRing R] [AddCommGroup M] [Module R M]
 
 theorem ι_mul_ι (r₁ r₂) : ι (0 : QuadraticForm R R) r₁ * ι (0 : QuadraticForm R R) r₂ = 0 := by
   rw [← mul_one r₁, ← mul_one r₂, ← smul_eq_mul R, ← smul_eq_mul R, LinearMap.map_smul,
-    LinearMap.map_smul, smul_mul_smul, ι_sq_scalar, QuadraticForm.zero_apply, RingHom.map_zero,
+    LinearMap.map_smul, smul_mul_smul, ι_sq_scalar, QuadraticMap.zero_apply, RingHom.map_zero,
     smul_zero]
 #align clifford_algebra_dual_number.ι_mul_ι CliffordAlgebraDualNumber.ι_mul_ι
 
@@ -415,14 +416,14 @@ protected def equiv : CliffordAlgebra (0 : QuadraticForm R R) ≃ₐ[R] R[ε] :=
     (by
       ext : 1
       -- This used to be a single `simp` before leanprover/lean4#2644
-      simp only [QuadraticForm.zero_apply, AlgHom.coe_comp, Function.comp_apply, lift_apply_eps,
+      simp only [QuadraticMap.zero_apply, AlgHom.coe_comp, Function.comp_apply, lift_apply_eps,
         AlgHom.coe_id, id_eq]
       erw [lift_ι_apply]
       simp)
     -- This used to be a single `simp` before leanprover/lean4#2644
     (by
       ext : 2
-      simp only [QuadraticForm.zero_apply, AlgHom.comp_toLinearMap, LinearMap.coe_comp,
+      simp only [QuadraticMap.zero_apply, AlgHom.comp_toLinearMap, LinearMap.coe_comp,
         Function.comp_apply, AlgHom.toLinearMap_apply, AlgHom.toLinearMap_id, LinearMap.id_comp]
       erw [lift_ι_apply]
       simp)