Commit 2024-01-08 16:53 dfdfce56

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 in SesquilinearForm
• Reduce duplication of argument between the two files
• Validate that the results in SesquilinearForm are sufficiently general to provide the results in BilinearForm in their existing form - in fact, some loosening of the hypothesis in SesquilinearForm is required. Further loosening was already applied in #9475