New issue
Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.
By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.
Already on GitHub? Sign in to your account
[Merged by Bors] - refactor(LinearAlgebra/QuadraticForm): Replace BilinForm
with a scalar valued bi LinearMap
#10238
Conversation
!bench |
Here are the benchmark results for commit 1fe7c06. Benchmark Metric Change
=====================================================================================
+ ~Mathlib.LinearAlgebra.CliffordAlgebra.BaseChange instructions -14.2%
- ~Mathlib.LinearAlgebra.QuadraticForm.Basic instructions 30.0%
- ~Mathlib.LinearAlgebra.QuadraticForm.TensorProduct instructions 57.9%
+ ~Mathlib.LinearAlgebra.QuadraticForm.TensorProduct.Isometries instructions -12.5% |
This PR/issue depends on: |
bors d+ Thanks for this, it now looks excellent! |
✌️ mans0954 can now approve this pull request. To approve and merge a pull request, simply reply with |
bors r+ |
…lar 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. Co-authored-by: Eric Wieser <wieser.eric@gmail.com> Co-authored-by: Christopher Hoskin <christopher.hoskin@overleaf.com>
Pull request successfully merged into master. Build succeeded: |
BilinForm
with a scalar valued bi LinearMap
BilinForm
with a scalar valued bi LinearMap
…lar 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. Co-authored-by: Eric Wieser <wieser.eric@gmail.com> Co-authored-by: Christopher Hoskin <christopher.hoskin@overleaf.com>
…lar 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. Co-authored-by: Eric Wieser <wieser.eric@gmail.com> Co-authored-by: Christopher Hoskin <christopher.hoskin@overleaf.com>
…lar 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. Co-authored-by: Eric Wieser <wieser.eric@gmail.com> Co-authored-by: Christopher Hoskin <christopher.hoskin@overleaf.com>
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 throughoutLinearAlgebra/QuadraticForm/
. Minor changes are also required elsewhere:LinearAlgebra/CliffordAlgebra/
LinearAlgebra/Matrix/PosDef
LinearAlgebra/SesquilinearForm