You signed in with another tab or window. Reload to refresh your session.You signed out in another tab or window. Reload to refresh your session.You switched accounts on another tab or window. Reload to refresh your session.Dismiss alert
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
Co-authored-by: Christopher Hoskin <mans0954@users.noreply.github.com>
Co-authored-by: Christopher Hoskin <christopher.hoskin@overleaf.com>
0 commit comments