-
Notifications
You must be signed in to change notification settings - Fork 331
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/Basic) : Generalise QuadraticForm
to QuadraticMap
#7569
Conversation
Having thought some more, I think the non-commutative case should be |
I had that thought too - the polar would be a σ-sesquilinear form. |
General information:
15 files got slower by at least 10⁹ instructions
6 files got slower by at least 10%:
No file got faster by at least 10⁹ instructions. No file got faster by at least 10%. |
bors d+ Thanks again for your patience here! Please look over @MichaelStollBayreuth's suggestions above, and reword the docstrings where appropriate. The performance doesn't look great (especially impacting files that I spend time on!), but I think this is likely just an unavoidable cost of generality, and so we don't need to worry about it for now. |
✌️ mans0954 can now approve this pull request. To approve and merge a pull request, simply reply with |
Co-authored-by: Michael Stoll <[email protected]>
Co-authored-by: Michael Stoll <[email protected]>
Co-authored-by: Eric Wieser <[email protected]>
Co-authored-by: Eric Wieser <[email protected]>
Co-authored-by: Michael Stoll <[email protected]>
Co-authored-by: Michael Stoll <[email protected]>
Co-authored-by: Michael Stoll <[email protected]>
Co-authored-by: Michael Stoll <[email protected]>
Co-authored-by: Michael Stoll <[email protected]>
Co-authored-by: Michael Stoll <[email protected]>
Co-authored-by: Michael Stoll <[email protected]>
bors r+ |
…rm` to `QuadraticMap` (#7569) Most of the theory in `LinearAlgebra/QuadraticForm/Basic` also holds for Quadratic Maps with minimal modification. A quadratic form is just a special case of a quadratic map. To keep this PR to a reasonable size I have not attempted to generalise other files in `LinearAlgebra/QuadraticForm` - this can be done in subsequent PRs. To facilitate dot notation we also introduce `LinearMap.BilinMap` as an abbreviation for `M →ₗ[R] M →ₗ[R] N`. No attempt has been made to generalise all `BilinForm` results to `BilinMap` at this stage. Some results in `LinearAlgebra/QuadraticForm/Basic` are still stated for quadratic forms either because there was no obvious generalisation to quadratic maps, or the generalisation requires improvements elsewhere in Mathlib which can be considered in subsequent PRs. My motivation for introducing Quadratic Maps to Mathlib is that it would allow the definition of interesting non-associative structures such as quadratic Jordan Algebras and Jordan Pairs. Co-authored-by: Eric Wieser <[email protected]> Co-authored-by: Christopher Hoskin <[email protected]> Co-authored-by: Christopher Hoskin <[email protected]>
Pull request successfully merged into master. Build succeeded: |
QuadraticForm
to QuadraticMap
QuadraticForm
to QuadraticMap
Also `.prod` and `.pi`, since these are heavily entangled with `Isometry` and `IsometryEquiv`. Follows on from #7569.
Most of the theory in
LinearAlgebra/QuadraticForm/Basic
also holds for Quadratic Maps with minimal modification. A quadratic form is just a special case of a quadratic map.To keep this PR to a reasonable size I have not attempted to generalise other files in
LinearAlgebra/QuadraticForm
- this can be done in subsequent PRs.To facilitate dot notation we also introduce
LinearMap.BilinMap
as an abbreviation forM →ₗ[R] M →ₗ[R] N
. No attempt has been made to generalise allBilinForm
results toBilinMap
at this stage.Some results in
LinearAlgebra/QuadraticForm/Basic
are still stated for quadratic forms either because there was no obvious generalisation to quadratic maps, or the generalisation requires improvements elsewhere in Mathlib which can be considered in subsequent PRs.My motivation for introducing Quadratic Maps to Mathlib is that it would allow the definition of interesting non-associative structures such as quadratic Jordan Algebras and Jordan Pairs.