Commit 2023-08-25 10:49 0d2b1239

View on Github →

feat(LinearAlgebra/QuadraticForm/TensorProduct): base change of quadratic forms (#6636)

Estimated changes

Modified Mathlib.lean

Modified Mathlib/LinearAlgebra/QuadraticForm/Basic.lean

added theorem QuadraticForm.associated_sq

Created Mathlib/LinearAlgebra/QuadraticForm/TensorProduct.lean

added theorem QuadraticForm.associated_baseChange

added theorem QuadraticForm.associated_tmul

added theorem QuadraticForm.baseChange_tmul

added def QuadraticForm.tensorDistrib

added theorem QuadraticForm.tensorDistrib_tmul