[Merged by Bors] - feat: add some simple results regarding polynomials #10572
Add this suggestion to a batch that can be applied as a single commit.
This suggestion is invalid because no changes were made to the code.
Suggestions cannot be applied while the pull request is closed.
Suggestions cannot be applied while viewing a subset of changes.
Only one suggestion per line can be applied in a batch.
Add this suggestion to a batch that can be applied as a single commit.
Applying suggestions on deleted lines is not supported.
You must change the existing code in this line in order to create a valid suggestion.
Outdated suggestions cannot be applied.
This suggestion has been applied or marked resolved.
Suggestions cannot be applied from pending reviews.
Suggestions cannot be applied on multi-line comments.
Suggestions cannot be applied while the pull request is queued to merge.
Suggestion cannot be applied right now. Please check back later.
Polynomial.map_contract
:Polynomial.map
andPolynomial.contract
commutesIrreducible.natDegree_pos
: an irreducible polynomial over a field must have positive degree (not true if it's not a field)Polynomial.Monic.nextCoeff_pow
: corollary ofPolynomial.Monic.nextCoeff_mul
Polynomial.exists_monic_irreducible_factor
: a polynomial over a field which is not a unit must have a monic irreducible factor (not true if it's not a field)