Commit 2025-01-25 23:10 e137b58e

View on Github →

feat: add QuadraticMap.associated_tmul and thus golf QuadraticForm.associated_tmul (#20177)

Estimated changes

Modified Mathlib/LinearAlgebra/BilinearForm/TensorProduct.lean

added theorem LinearMap.BilinMap.baseChange_isSymm

added theorem LinearMap.BilinMap.tmul_isSymm

Modified Mathlib/LinearAlgebra/QuadraticForm/Basic.lean

added theorem QuadraticForm.associated_isSymm

modified theorem QuadraticMap.associated_isSymm

modified theorem QuadraticMap.associated_left_inverse

modified theorem QuadraticMap.isSymm_toMatrix'

Modified Mathlib/LinearAlgebra/QuadraticForm/TensorProduct.lean

added theorem QuadraticMap.associated_tmul

Modified Mathlib/LinearAlgebra/SesquilinearForm.lean

added theorem LinearMap.BilinMap.isSymm_iff_eq_flip

modified theorem LinearMap.isSymm_iff_eq_flip