Commit 2023-09-18 15:32 d9e7e897

View on Github →

feat(LinearAlgebra/QuadraticForm/TensorProduct): commutativity and associativity (#7223) This was discussed at LFTCM regarding the Grothendieck-Witt ring of quadratic forms. These could eventually be used to show that #6987 forms a braided monoidal category.

Estimated changes

Modified Mathlib.lean

Modified Mathlib/LinearAlgebra/BilinearForm.lean

added theorem LinearMap.toBilin_apply

Modified Mathlib/LinearAlgebra/QuadraticForm/Basic.lean

added theorem QuadraticForm.polarBilin_comp

added theorem QuadraticForm.polarBilin_injective

added theorem QuadraticForm.toQuadraticForm_polarBilin

Created Mathlib/LinearAlgebra/QuadraticForm/TensorProduct/Isometries.lean

added def QuadraticForm.Isometry.tmul

added theorem QuadraticForm.Isometry.tmul_apply

added theorem QuadraticForm.comp_tensorLId_eq

added theorem QuadraticForm.comp_tensorRId_eq

added def QuadraticForm.tensorAssoc

added theorem QuadraticForm.tensorAssoc_apply

added theorem QuadraticForm.tensorAssoc_symm_apply

added def QuadraticForm.tensorComm

added theorem QuadraticForm.tensorComm_apply

added theorem QuadraticForm.tensorComm_symm

added def QuadraticForm.tensorLId

added theorem QuadraticForm.tensorLId_apply

added theorem QuadraticForm.tensorLId_symm_apply

added def QuadraticForm.tensorRId

added theorem QuadraticForm.tensorRId_apply

added theorem QuadraticForm.tensorRId_symm_apply

added theorem QuadraticForm.tmul_comp_tensorAssoc

added theorem QuadraticForm.tmul_comp_tensorComm

added theorem QuadraticForm.tmul_comp_tensorMap

added theorem QuadraticForm.tmul_tensorAssoc_apply

added theorem QuadraticForm.tmul_tensorComm_apply

added theorem QuadraticForm.tmul_tensorLId_apply

added theorem QuadraticForm.tmul_tensorMap_apply

added theorem QuadraticForm.tmul_tensorRId_apply