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] - feat(field_theory/splitting_field): generalize some results from field to domain #10726
Conversation
@alexjbest I pushed a refactor. By now it might make sense to reorganize properly into a section with variables. |
@@ -422,6 +426,48 @@ calc ((roots ((X : polynomial R) ^ n - C a)).card : with_bot ℕ) | |||
≤ degree ((X : polynomial R) ^ n - C a) : card_roots (X_pow_sub_C_ne_zero hn a) | |||
... = n : degree_X_pow_sub_C hn a | |||
|
|||
lemma le_root_multiplicity_map {K L : Type*} [comm_ring K] [is_domain K] | |||
[comm_ring L] [is_domain L] {p : polynomial K} {f : K →+* L} (hf : function.injective f) |
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.
I different version might assume map f p ≠ 0
instead of function.injective f
.
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.
Shall we add a ' version then (or of map_ne_zero)?
@jcommelin |
… alexjbest/generalize_field_div
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.
Thanks 🎉
bors merge
merge conflict |
Canceled. |
bors d+ |
✌️ alexjbest can now approve this pull request. To approve and merge a pull request, simply reply with |
… alexjbest/generalize_field_div
bors r+ |
…d to domain (#10726) This PR does a few things generalizing / golfing facts related to polynomials and splitting fields. - Generalize some results in `data.polynomial.field_division` to division rings - generalize `C_leading_coeff_mul_prod_multiset_X_sub_C` from a field to a domain - same for `prod_multiset_X_sub_C_of_monic_of_roots_card_eq` - add a supporting useful lemma `roots_map_of_injective_card_eq_total_degree` saying that if we already have a full (multi)set of roots over a domain, passing along an injection gives the set of roots of the mapped polynomial Inspired by needs of flt-regular. Co-authored-by: Johan Commelin <johan@commelin.net>
Pull request successfully merged into master. Build succeeded: |
This PR does a few things generalizing / golfing facts related to polynomials and splitting fields.
data.polynomial.field_division
to division ringsC_leading_coeff_mul_prod_multiset_X_sub_C
from a field to a domainprod_multiset_X_sub_C_of_monic_of_roots_card_eq
roots_map_of_injective_card_eq_total_degree
saying that if we already have a full (multi)set of roots over a domain, passing along an injection gives the set of roots of the mapped polynomialInspired by needs of flt-regular.