[Merged by Bors] - refactor(LinearAlgebra/QuadraticForm/Basic) : Generalise QuadraticForm to QuadraticMap

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)