Commit 2025-08-10 16:17 a7e5d7b0

View on Github →

chore: turn LinearMap.IsSymm into a structure (#27873) This is to allow extending the structure to define positive semidefinite sesquilinear forms in #28052, similarly to what was done in #26274.

Estimated changes

Modified Counterexamples/QuadraticForm.lean

modified theorem Counterexample.isSymm_B

Modified Mathlib/Algebra/Lie/TraceForm.lean

modified theorem LieModule.traceForm_isSymm

Modified Mathlib/LinearAlgebra/BilinearForm/Properties.lean

Modified Mathlib/LinearAlgebra/BilinearForm/TensorProduct.lean

Modified Mathlib/LinearAlgebra/QuadraticForm/Basic.lean

Modified Mathlib/LinearAlgebra/QuadraticForm/Dual.lean

modified theorem LinearMap.isSymm_dualProd

Modified Mathlib/LinearAlgebra/RootSystem/Finite/CanonicalBilinear.lean

Modified Mathlib/LinearAlgebra/RootSystem/OfBilinear.lean

Modified Mathlib/LinearAlgebra/RootSystem/RootPositive.lean

Modified Mathlib/LinearAlgebra/SesquilinearForm.lean

modified theorem LinearMap.IsSymm.domRestrict

added structure LinearMap.IsSymm

deleted def LinearMap.IsSymm

added theorem LinearMap.isSymm_def

modified theorem LinearMap.isSymm_zero