Commit 2024-01-08 16:53 dfdfce56
View on Github →refactor(LinearAlgebra/Matrix/BilinearForm): Derive BilinearForm results from SesquilinearForm (#9485)
Give definitions in LinearAlgebra/Matrix/BilinearForm
in terms of the equivalent definitions in LinearAlgebra/Matrix/SesquilinearForm
and derive the BilinearForm
results as effectively special cases of the equivalent results in SesquilinearForm
. This reduces the length of LinearAlgebra/Matrix/BilinearForm
by over 100 lines.
The aim is to:
- Clarify how results in
BilinearForm
relate to results inSesquilinearForm
- Reduce duplication of argument between the two files
- Validate that the results in
SesquilinearForm
are sufficiently general to provide the results inBilinearForm
in their existing form - in fact, some loosening of the hypothesis inSesquilinearForm
is required. Further loosening was already applied in #9475