[Merged by Bors] - feat(data/polynomial/degree): lemmas on nat_degree and behaviour under multiplication by constants #6224
Conversation
These lemmas extend the API for nat_degree I intend to use them to work with integrality statements
| ... = f.nat_degree + 0 : by rw nat_degree_C a | ||
| ... = f.nat_degree : add_zero _ | ||
|
|
||
| lemma nat_degree_mul_C_eq_of_mul_eq_one {ai : R} (au : a * ai = 1) {f : polynomial R} : |
There was a problem hiding this comment.
These lemmas hold more generally for \forall ai, ai * a \ne 0 right? In particular, that hypothesis means you can create a simpler lemma for no_zero_divisors
There was a problem hiding this comment.
I am on my phone, so I may be misunderstanding. I agree that it suffices to assume that a is a non-zero divisor and I could prove it in this case, adding then a lemma saying that having an inverse implies being a non-zero divisor. However, assuming every non-zero element of R is a non-zero divisor is more than I want.
There was a problem hiding this comment.
I'm suggesting both - show that it suffices for a to be a nonzero divisor, but for convenience, also provide the lemma that provides that hypothesis automatically from the fact that it is true for all a using typeclass search when working in the reals, rationals, etc
There was a problem hiding this comment.
Eric, I decided to add a more direct lemma, assuming that the product a * f.leading_coeff does not vanish. This implies quickly the result that you want about non-zero divisors. The proofs of the results that I needed, though, have not been affected.
I also found out that the final section on no_zero_divisors assumed comm_semiring and I removed the comm assumption: let's see if mathlib likes this! If it does not, I will add the hypothesis back and that refactor will wait a separate PR.
…er-community/mathlib into adomani_nat_degree_inequalities
move lemmas to the right section
| /-- Although not explicitly stated, the assumptions of this lemma force the polynomial `p` to be | ||
| non-zero, via `p.leading_coeff ≠ 0`. The lemmas below split cases, effectively removing this | ||
| assumption in some cases. | ||
| -/ | ||
| lemma nat_degree_mul_C_eq_of_mul_ne_zero (h : p.leading_coeff * a ≠ 0) : | ||
| (p * C a).nat_degree = p.nat_degree := | ||
| begin | ||
| refine eq_nat_degree_of_le_mem_support (nat_degree_mul_C_le p a) _, | ||
| refine mem_support_iff_coeff_ne_zero.mpr _, | ||
| rwa coeff_mul_C, | ||
| end | ||
|
|
||
| /-- Although not explicitly stated, the assumptions of this lemma force the polynomial `p` to be | ||
| non-zero, via `p.leading_coeff ≠ 0`. The lemmas below split cases, effectively removing this | ||
| assumption in some cases. | ||
| -/ | ||
| lemma nat_degree_C_mul_eq_of_mul_ne_zero (h : a * p.leading_coeff ≠ 0) : |
There was a problem hiding this comment.
Can you explicitly name the lemmas you're referring to here, so that they link in doc-gen?
There was a problem hiding this comment.
Done! Thanks for the suggestion!
adomani
added
the
awaiting-review
|
I question about the more general structure... the file is |
|
Johan, I like your suggestion and I agree that this file is getting long. I am happy to simply move these lemmas somewhere else, but your suggestion seems to imply a larger migration. I do not have a criterion, though, for which lemmas belong to "definitions" and which to "lemmas". If you have some guidance, I can move the lemmas of this PR, along with some of the ones that are already misplaced, in their correct home. |
|
I moved the new lemmas from I still agree that having shorter files is desirable. In more geometric/topological arguments, the theory is often split into "properties about a single point" and "properties about more than one point". The first class contains all the local stuff (e.g. filters, neighbourhoods); the second class contains "relative" properties (e.g. separation axioms). We could try a similar split, with lemmas whose statement is about a single polynomial on one side and lemmas with more than one polynomial in their statement. I imagine that such a clean cut will not be possible, but it may inform a strategy. What do you think? |
|
I think this looks great for now, thanks @adomani ! If there's more refactoring to be done, maybe another PR is welcome. I don't know the ideal way to split this stuff up. Maybe worth a Zulip thread. bors merge |
github-actions
bot
added
ready-to-merge
…r multiplication by constants (#6224) These lemmas extend the API for nat_degree I intend to use them to work with integrality statements
|
Rob, thanks! I have not given the splitting more thought, so for the moment, I am happy like this! |
|
Pull request successfully merged into master. Build succeeded: |
bors
bot
changed the title
…r multiplication by constants (#6224) These lemmas extend the API for nat_degree I intend to use them to work with integrality statements
These lemmas extend the API for nat_degree
I intend to use them to work with integrality statements