chore(LinearAlgebra): remove workarounds for compilation performance issues (#26786)

eric-wieser · eric-wieser · commit 3bcc451cb50c · 2025-07-05T22:35:30.000Z
#7103 is resolved by the new compiler, at least for everything in this PR.
diff --git a/Mathlib/Algebra/Category/ModuleCat/Monoidal/Basic.lean b/Mathlib/Algebra/Category/ModuleCat/Monoidal/Basic.lean
@@ -27,9 +27,6 @@ If you're happy using the bundled `ModuleCat R`, it may be possible to mostly
 use this as an interface and not need to interact much with the implementation details.
 -/
 
-
-suppress_compilation
-
 universe v w x u
 
 open CategoryTheory
@@ -230,7 +227,7 @@ variable (f : M₁ → M₂ → M₃) (h₁ : ∀ m₁ m₂ n, f (m₁ + m₂) n
   (h₄ : ∀ (a : R) m n, f m (a • n) = a • f m n)
 
 /-- Construct for morphisms from the tensor product of two objects in `ModuleCat`. -/
-noncomputable def tensorLift : M₁ ⊗ M₂ ⟶ M₃ :=
+def tensorLift : M₁ ⊗ M₂ ⟶ M₃ :=
   ofHom <| TensorProduct.lift (LinearMap.mk₂ R f h₁ h₂ h₃ h₄)
 
 @[simp]
diff --git a/Mathlib/Algebra/Category/ModuleCat/Monoidal/Closed.lean b/Mathlib/Algebra/Category/ModuleCat/Monoidal/Closed.lean
@@ -11,8 +11,6 @@ import Mathlib.Algebra.Category.ModuleCat.Monoidal.Symmetric
 # The monoidal closed structure on `Module R`.
 -/
 
-suppress_compilation
-
 universe v w x u
 
 open CategoryTheory Opposite
diff --git a/Mathlib/Algebra/Category/ModuleCat/Monoidal/Symmetric.lean b/Mathlib/Algebra/Category/ModuleCat/Monoidal/Symmetric.lean
@@ -10,8 +10,6 @@ import Mathlib.Algebra.Category.ModuleCat.Monoidal.Basic
 # The symmetric monoidal structure on `Module R`.
 -/
 
-suppress_compilation
-
 universe v w x u
 
 open CategoryTheory MonoidalCategory
diff --git a/Mathlib/LinearAlgebra/CliffordAlgebra/BaseChange.lean b/Mathlib/LinearAlgebra/CliffordAlgebra/BaseChange.lean
@@ -42,8 +42,7 @@ namespace CliffordAlgebra
 variable (A)
 
 /-- Auxiliary construction: note this is really just a heterobasic `CliffordAlgebra.map`. -/
--- `noncomputable` is a performance workaround for https://github.com/leanprover-community/mathlib4/issues/7103
-noncomputable def ofBaseChangeAux (Q : QuadraticForm R V) :
+def ofBaseChangeAux (Q : QuadraticForm R V) :
     CliffordAlgebra Q →ₐ[R] CliffordAlgebra (Q.baseChange A) :=
   CliffordAlgebra.lift Q <| by
     refine ⟨(ι (Q.baseChange A)).restrictScalars R ∘ₗ TensorProduct.mk R A V 1, fun v => ?_⟩
@@ -57,8 +56,7 @@ noncomputable def ofBaseChangeAux (Q : QuadraticForm R V) :
 
 /-- Convert from the base-changed clifford algebra to the clifford algebra over a base-changed
 module. -/
--- `noncomputable` is a performance workaround for https://github.com/leanprover-community/mathlib4/issues/7103
-noncomputable def ofBaseChange (Q : QuadraticForm R V) :
+def ofBaseChange (Q : QuadraticForm R V) :
     A ⊗[R] CliffordAlgebra Q →ₐ[A] CliffordAlgebra (Q.baseChange A) :=
   Algebra.TensorProduct.lift (Algebra.ofId _ _) (ofBaseChangeAux A Q)
     fun _a _x => Algebra.commutes _ _
@@ -76,8 +74,7 @@ noncomputable def ofBaseChange (Q : QuadraticForm R V) :
 
 /-- Convert from the clifford algebra over a base-changed module to the base-changed clifford
 algebra. -/
--- `noncomputable` is a performance workaround for https://github.com/leanprover-community/mathlib4/issues/7103
-noncomputable def toBaseChange (Q : QuadraticForm R V) :
+def toBaseChange (Q : QuadraticForm R V) :
     CliffordAlgebra (Q.baseChange A) →ₐ[A] A ⊗[R] CliffordAlgebra Q :=
   CliffordAlgebra.lift _ <| by
     refine ⟨TensorProduct.AlgebraTensorModule.map (LinearMap.id : A →ₗ[A] A) (ι Q), ?_⟩
@@ -179,8 +176,7 @@ base-changing the clifford algebra itself; <|Cℓ(A ⊗_R V, Q_A) ≅ A ⊗_R C
 
 This is `CliffordAlgebra.toBaseChange` and `CliffordAlgebra.ofBaseChange` as an equivalence. -/
 @[simps!]
--- `noncomputable` is a performance workaround for https://github.com/leanprover-community/mathlib4/issues/7103
-noncomputable def equivBaseChange (Q : QuadraticForm R V) :
+def equivBaseChange (Q : QuadraticForm R V) :
     CliffordAlgebra (Q.baseChange A) ≃ₐ[A] A ⊗[R] CliffordAlgebra Q :=
   AlgEquiv.ofAlgHom (toBaseChange A Q) (ofBaseChange A Q)
     (toBaseChange_comp_ofBaseChange A Q)
diff --git a/Mathlib/LinearAlgebra/QuadraticForm/QuadraticModuleCat/Monoidal.lean b/Mathlib/LinearAlgebra/QuadraticForm/QuadraticModuleCat/Monoidal.lean
@@ -24,8 +24,6 @@ For now, we simplify by insisting both universe levels are the same.
 This file essentially mirrors `Mathlib/Algebra/Category/AlgCat/Monoidal.lean`.
 -/
 
-suppress_compilation
-
 open CategoryTheory
 open scoped MonoidalCategory
 
@@ -41,13 +39,13 @@ namespace instMonoidalCategory
 
 /-- Auxiliary definition used to build `QuadraticModuleCat.instMonoidalCategory`. -/
 @[simps! form]
-noncomputable abbrev tensorObj (X Y : QuadraticModuleCat.{u} R) : QuadraticModuleCat.{u} R :=
+abbrev tensorObj (X Y : QuadraticModuleCat.{u} R) : QuadraticModuleCat.{u} R :=
   of (X.form.tmul Y.form)
 
 /-- Auxiliary definition used to build `QuadraticModuleCat.instMonoidalCategory`.
 
 We want this up front so that we can re-use it to define `whiskerLeft` and `whiskerRight`. -/
-noncomputable abbrev tensorHom {W X Y Z : QuadraticModuleCat.{u} R} (f : W ⟶ X) (g : Y ⟶ Z) :
+abbrev tensorHom {W X Y Z : QuadraticModuleCat.{u} R} (f : W ⟶ X) (g : Y ⟶ Z) :
     tensorObj W Y ⟶ tensorObj X Z :=
   ⟨f.toIsometry.tmul g.toIsometry⟩
 
@@ -79,7 +77,7 @@ theorem forget₂_map_associator_inv (X Y Z : QuadraticModuleCat.{u} R) :
     (forget₂ (QuadraticModuleCat R) (ModuleCat R)).map (α_ X Y Z).inv =
       (α_ X.toModuleCat Y.toModuleCat Z.toModuleCat).inv := rfl
 
-noncomputable instance instMonoidalCategory : MonoidalCategory (QuadraticModuleCat.{u} R) :=
+instance instMonoidalCategory : MonoidalCategory (QuadraticModuleCat.{u} R) :=
   Monoidal.induced
     (forget₂ (QuadraticModuleCat R) (ModuleCat R))
     { μIso := fun _ _ => Iso.refl _
diff --git a/Mathlib/LinearAlgebra/QuadraticForm/QuadraticModuleCat/Symmetric.lean b/Mathlib/LinearAlgebra/QuadraticForm/QuadraticModuleCat/Symmetric.lean
@@ -18,8 +18,6 @@ In this file we show:
 This file essentially mirrors `Mathlib/Algebra/Category/AlgCat/Symmetric.lean`.
 -/
 
-suppress_compilation
-
 open CategoryTheory
 
 universe v u
diff --git a/Mathlib/LinearAlgebra/QuadraticForm/TensorProduct.lean b/Mathlib/LinearAlgebra/QuadraticForm/TensorProduct.lean
@@ -40,8 +40,7 @@ variable (R A) in
 
 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 https://github.com/leanprover-community/mathlib4/issues/7103
-noncomputable def tensorDistrib :
+def tensorDistrib :
     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
@@ -61,8 +60,7 @@ theorem tensorDistrib_tmul (Q₁ : QuadraticMap A M₁ N₁) (Q₂ : QuadraticMa
     (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 https://github.com/leanprover-community/mathlib4/issues/7103
-protected noncomputable abbrev tmul (Q₁ : QuadraticMap A M₁ N₁)
+protected 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₂)
 
@@ -84,8 +82,7 @@ variable (R A) in
 
 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 https://github.com/leanprover-community/mathlib4/issues/7103
-noncomputable def tensorDistrib :
+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
 
@@ -99,8 +96,7 @@ theorem tensorDistrib_tmul (Q₁ : QuadraticForm A M₁) (Q₂ : QuadraticForm R
     (associated_eq_self_apply _ _ _) (associated_eq_self_apply _ _ _)
 
 /-- The tensor product of two quadratic forms, a shorthand for dot notation. -/
--- `noncomputable` is a performance workaround for https://github.com/leanprover-community/mathlib4/issues/7103
-protected noncomputable abbrev tmul (Q₁ : QuadraticForm A M₁) (Q₂ : QuadraticForm R M₂) :
+protected abbrev tmul (Q₁ : QuadraticForm A M₁) (Q₂ : QuadraticForm R M₂) :
     QuadraticForm A (M₁ ⊗[R] M₂) :=
   tensorDistrib R A (Q₁ ⊗ₜ[R] Q₂)
 
@@ -119,8 +115,7 @@ theorem polarBilin_tmul [Invertible (2 : A)] (Q₁ : QuadraticForm A M₁) (Q₂
 
 variable (A) in
 /-- The base change of a quadratic form. -/
--- `noncomputable` is a performance workaround for https://github.com/leanprover-community/mathlib4/issues/7103
-protected noncomputable def baseChange (Q : QuadraticForm R M₂) : QuadraticForm A (A ⊗[R] M₂) :=
+protected def baseChange (Q : QuadraticForm R M₂) : QuadraticForm A (A ⊗[R] M₂) :=
   QuadraticForm.tmul (R := R) (A := A) (M₁ := A) (M₂ := M₂) (QuadraticMap.sq (R := A)) Q
 
 @[simp]
