Commit 2024-02-08 05:11 922e827c

View on Github →

chore(LinearAlgebra/QuadraticForm): fixups to #10097 (#10167) I didn't get a chance to review #10097 before it was merged; this contains some minor fixups. This removes LinearMap.linMulLin, as it can be recovered easily via LinearMap.mul.

Estimated changes

Modified Mathlib/Algebra/Algebra/Bilinear.lean

added def LinearMap.restrictScalars₁₂

Modified Mathlib/LinearAlgebra/BilinearMap.lean

deleted def LinearMap.linMulLin

Modified Mathlib/LinearAlgebra/QuadraticForm/Basic.lean

modified def BilinForm.toQuadraticFormLinearMap

modified def LinearMap.toQuadraticForm

modified def QuadraticForm.weightedSumSquares