Commit 2024-02-26 00:38 9f926b1a

View on Github →

refactor(LinearAlgebra/QuadraticForm): Replace BilinForm with a scalar valued bi LinearMap (#10238) Following on from #10097, which converted the companion of a quadratic form with a bilinear map, this PR replaces a number of results about quadratic forms and bilinear forms with results about quadratic forms and scalar valued bilinear maps. The long term aim is to be able to consider quadratic maps. The main change is to LinearAlgebra/QuadraticForm/Basic, but this necessitates changes throughout LinearAlgebra/QuadraticForm/. Minor changes are also required elsewhere:

  • LinearAlgebra/CliffordAlgebra/
  • LinearAlgebra/Matrix/PosDef
  • LinearAlgebra/SesquilinearForm
  • A number of additional results about tensor products and linear maps are also required.

Estimated changes

modified theorem Counterexample.B_ne_zero
deleted theorem BilinForm.IsSymm.tmul
deleted theorem BilinForm.baseChange_tmul
added theorem LinearMap.IsSymm.tmul
modified theorem QuadraticForm.associated_sq
modified def LinearMap.dualProd
added theorem LinearMap.isSymm_zero