Commit 2023-10-09 13:35 281dea7c

View on Github →

refactor(LinearAlgebra/QuadraticForm/Basic): remove non-commutativity support (#7581) As discussed on Zulip, this generalization seems nonsensical as currently implemented. There are sensible ways to make this generalization, but they are much larger refactors, and in the meantime the current generalization is useless anyway.

Estimated changes

Modified Counterexamples/QuadraticForm.lean

Modified Mathlib/LinearAlgebra/CliffordAlgebra/Contraction.lean

Modified Mathlib/LinearAlgebra/Matrix/PosDef.lean

Modified Mathlib/LinearAlgebra/QuadraticForm/Basic.lean

modified def Matrix.toQuadraticForm'

modified theorem QuadraticForm.associated_linMulLin

modified theorem QuadraticForm.associated_sq

modified theorem QuadraticForm.basisRepr_eq_of_iIsOrtho

modified def QuadraticForm.discr

modified theorem QuadraticForm.discr_comp

modified theorem QuadraticForm.discr_smul

modified theorem QuadraticForm.isSymm_toMatrix'

modified theorem QuadraticForm.polar_comp

modified def QuadraticForm.toMatrix'

modified theorem QuadraticForm.toMatrix'_comp

modified theorem QuadraticForm.toMatrix'_smul

modified def QuadraticForm.weightedSumSquares

modified theorem QuadraticForm.weightedSumSquares_apply

modified structure QuadraticForm

Modified Mathlib/LinearAlgebra/QuadraticForm/Complex.lean

Modified Mathlib/LinearAlgebra/QuadraticForm/Isometry.lean

Modified Mathlib/LinearAlgebra/QuadraticForm/IsometryEquiv.lean

Modified Mathlib/LinearAlgebra/QuadraticForm/Prod.lean

modified theorem QuadraticForm.PosDef.prod

modified theorem QuadraticForm.anisotropic_of_pi

modified theorem QuadraticForm.anisotropic_of_prod

modified theorem QuadraticForm.nonneg_pi_iff

modified theorem QuadraticForm.nonneg_prod_iff

modified theorem QuadraticForm.posDef_pi_iff

modified theorem QuadraticForm.posDef_prod_iff

Modified Mathlib/LinearAlgebra/QuadraticForm/Real.lean

Modified Mathlib/LinearAlgebra/QuadraticForm/TensorProduct.lean