Commit 2025-07-05 22:35 3bcc451c

View on Github →

chore(LinearAlgebra): remove workarounds for compilation performance issues (#26786) https://github.com/leanprover-community/mathlib4/issues/7103 is resolved by the new compiler, at least for everything in this PR.

Estimated changes

Modified Mathlib/Algebra/Category/ModuleCat/Monoidal/Basic.lean

added def ModuleCat.MonoidalCategory.tensorLift

Modified Mathlib/Algebra/Category/ModuleCat/Monoidal/Closed.lean

Modified Mathlib/Algebra/Category/ModuleCat/Monoidal/Symmetric.lean

Modified Mathlib/LinearAlgebra/CliffordAlgebra/BaseChange.lean

added def CliffordAlgebra.equivBaseChange

added def CliffordAlgebra.ofBaseChange

added def CliffordAlgebra.ofBaseChangeAux

added def CliffordAlgebra.toBaseChange

Modified Mathlib/LinearAlgebra/QuadraticForm/QuadraticModuleCat/Monoidal.lean

Modified Mathlib/LinearAlgebra/QuadraticForm/QuadraticModuleCat/Symmetric.lean

Modified Mathlib/LinearAlgebra/QuadraticForm/TensorProduct.lean

added def QuadraticForm.tensorDistrib

added def QuadraticMap.tensorDistrib