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(linear_algebra/quadratic_form/basic): generalize to semiring #14303
Conversation
…to eric-wieser/quadratic_form-semiring
…gebra/quadratic_form/basic` 150 lines seems worthy of its own file, especially if this grows `fun_like` boilerplate in future. No lemmas have been renamed or proofs changed.
…com/leanprover-community/mathlib into eric-wieser/quadratic_form-semiring
…tic_form-semiring
784677c
to
7d1c233
Compare
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
LGTM! I just had one small question/comment for you to consider.
Also, it seems that the file quadratic_form/basic
is starting to get large, and trying to do too much. We should consider splitting it up (in a later PR). I think the basic defs should go in basic
while the anisotropic
stuff could go in a separate file called anisotropic
for example.
I completely agree! |
bors r+ |
…#14303) This uses a slightly nicer strategy than the one suggested by @adamtopaz [on Zulip](https://leanprover.zulipchat.com/#narrow/stream/116395-maths/topic/Exterior.20algebras.20over.20semiring/near/282808284). The main motivation here is to be able to talk about `0 : quadratic_form R M` even when there is no negation available, as that will let us merge `clifford_algebra` (which currently requires negation) and `exterior_algebra` (which does not). It's likely this generalization is broadly not very useful, so this adds a `quadratic_form.of_polar` constructor to preserve the old more convenient API. Note the `.bib` file changed slightly as I ran the autoformatting tool.
Pull request successfully merged into master. Build succeeded: |
This uses a slightly nicer strategy than the one suggested by @adamtopaz on Zulip.
The main motivation here is to be able to talk about
0 : quadratic_form R M
even when there is no negation available, as that will let us mergeclifford_algebra
(which currently requires negation) andexterior_algebra
(which does not).It's likely this generalization is broadly not very useful, so this adds a
quadratic_form.of_polar
constructor to preserve the old more convenient API.Note the
.bib
file changed slightly as I ran the autoformatting tool.linear_algebra/quadratic_form/basic
#14305