-
Notifications
You must be signed in to change notification settings - Fork 298
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
feat(field_theory/finite): cardinality of images of polynomials #1554
Conversation
... = _ : by rw [sum_const, add_monoid.smul_eq_mul', nat.cast_id] | ||
|
||
/-- If `f` and `g` are quadratic polynomials, then the `f.eval a + g.eval b = 0` has a solution. -/ | ||
lemma exists_root_sum_quadratic {f g : polynomial α} (hf2 : degree f = 2) |
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.
This seems closely related to the very useful https://en.wikipedia.org/wiki/Chevalley%E2%80%93Warning_theorem but I don't think it's a consequence. I certainly think that the lemma you formalised is useful outside of your direct application.
Would it make sense to have a version that uses the characteristic of alpha
instead of its cardinality mod 2?
|
||
open finset polynomial | ||
|
||
/-- The cardinality of a field is at most n times the cardinality of the image of a degree n |
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.
/-- The cardinality of a field is at most n times the cardinality of the image of a degree n | |
/-- The cardinality of a finite integral domain is at most n times the cardinality of the image of a degree n |
src/field_theory/finite.lean
Outdated
rcases hd with ⟨x, ⟨a, _, ha⟩, ⟨b, _, hb⟩⟩, | ||
use [a, b], | ||
rw [ha, ← hb, eval_neg, neg_add_self] | ||
end |
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.
This proof is long. But if you think you can't really split of useful sublemmas then I'm fine with merging this.
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.
Sadly I don't think there are any useful sublemmas. I shortened the proof a little.
…prover-community#1554) * feat(field_theory/finite): cardinality of images of polynomials * docstrings * Johan's suggestions * slightly shorten proof
One lemma about the cardinality of images of polynomials of roots of polynomials, and another about existence of roots of polynomials of a particular form over finite fields of odd cardinality.
These lemmas were used in a proof of the four squares theorem (every natural number is the sum of four squares, on Freek's list). They're difficult lemmas for the library, because they're not really textbook theorems, or theorems you might expect to find, but they still might be useful.
TO CONTRIBUTORS:
Make sure you have:
If this PR is related to a discussion on Zulip, please include a link in the discussion.
For reviewers: code review check list