feat(algebra/cubic_discriminant): remove custom cubic structure and replace by API about new to_poly
#15088
Conversation
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
mathlib-dependent-issues-bot
added
the
blocked-by-other-PR
vihdzp
reviewed
Jul 1, 2022
|
|
||
| lemma ne_zero_of_c_ne_zero (hc : P.c ≠ 0) : P.to_poly ≠ 0 := | ||
| (or_imp_distrib.mp (or_imp_distrib.mp (or_imp_distrib.mp ne_zero).2).2).1 hc | ||
| lemma coeff_to_poly_ge_four (P : fin N → R) (n : ℕ) (hn : N ≤ n) : (to_poly P).coeff n = 0 := |
There was a problem hiding this comment.
These new names are nonsense for anything other than a cubic polynomial.
|
|
||
| lemma degree_of_a_eq_zero (ha : P.a = 0) (hb : P.b ≠ 0) : P.to_poly.degree = 2 := | ||
| by rw [of_a_eq_zero ha, degree_quadratic hb] | ||
| lemma degree_to_poly_le : (to_poly P).degree ≤ N := |
There was a problem hiding this comment.
Can't you prove this with degree_to_poly_lt and nat.lt_succ_iff?
mathlib-dependent-issues-bot
removed
the
blocked-by-other-PR
4 tasks
semorrison
added
the
too-late
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
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.
Currently, the leaf file
algebra/cubic_discriminantby @Multramate introduces a customcubicstructure for polynomials of degree at most 3, which consists of a 4-tuple representing the coefficients plus some API.As far as I can tell, this structure would be just as useful if it worked for
N-tuples rather than just 4-tuples. So in this PR I introduce a constructor (temporarily namedto_poly, following the existing name for cubics) for a polynomial overRgiven a vectorfin N → Rof the coefficients, and switch thecubic_discriminantfile over to this, deleting thecubicstructure.If the idea is accepted as a good one, I will move the material about
to_polyout of thecubic_discriminantfile intodata/polynomialsomewhere. But for now, I am keeping everything inalgebra/cubic_discriminantto demonstrate that it at least has the merit of decreasing the length of that file by 40 lines.Zulip
polynomial.roots#14908The PR generalizes some of the existing results from cubics to arbitrary-length polynomials, which depends on a variant of Vieta's formulas, coincidentally recently PR'd. The diff of this PR is therefore large, but all the changes I propose are (temporarily) in the
cubic_discriminantfile.