feat(data/polynomial/degree): introduce reverse of a polynomial, prove reverse is multiplicative

[adomani]

---

[awainverse]

All the lemmas that don't have to do with polynomials shouldn't be in the data.polynomial directory, and certainly shouldn't be in the polynomial namespace.

[awainverse]

Thanks for all this work! I've wanted the reverse of a polynomial for a while.

I've left some fairly detailed reviews on some of the lemmas at the beginning of the file, trying to find suggestions for better names and homes for some of these lemmas.

However, there are a lot to go through, and this is a pretty long PR.
Do you think you could maybe break this into a few PRs?
I'd organize it based on which files you're adding the lemmas to.

[awainverse]

Put this next to degree_monomial, and maybe use that lemma for a shorter proof?

[awainverse]

We have some lemmas about this, in the form of finsupp.erase. I find it pretty useful, so I think it should have a definition that doesn't run into mild coercion problems you get from dealing with finsupps. However, there are definitely easier ways to define this polynomial, like using finsupp.erase, or probably better, f - C f.leading_coeff * X ^ f.nat_degree, so that your docstring is more literally true.

[adomani]

I did not know about the existence of erase. I thought of subtracting the leading coefficient, but that requires working with a ring, as opposed to a semiring, so I opted for getting rid of the support instead.

[adomani]

Dear Aaron,

thank you so much for your comments! Here is an itemized list of my reactions!

1. finset.card_pos and finset.min'_ne_max'_of_card solved all my issues with the initial lemmas, so I removed them.
2. I used not_mem_support_iff_coeff_zero.1 throughout.
3. I opted for using not_cong leading_coeff_eq_zero instead of leading_coeff_nonzero_of_nonzero.
4. Changed all terms to C_mul_X_pow.
5. Changed non_zero_iff to nonempty_support_iff and removed the partial implications, leaving only the equivalence.
6. Renamed defs_by_Johan as per your suggestion.
7. It turns out that I was not using nat_degree_monomial, so I removed it. However, using the lemma that you suggested, a proof is nat_degree_eq_of_degree_eq_some (degree_monomial n ha).
8. I changed the name using remove_leading_coefficient to erase_lead. I hope that this looks as an improvement to everyone!
9. I tried using erase for removing the leading coefficient, but with my implementation (that you can find below), the definition became noncomputable. I will therefore stick with a definition that I can make computable, if that is all right!

def erase_lead (f : polynomial R) : polynomial R := begin
  refine ⟨ f.support \ singleton f.nat_degree , finsupp.erase f.nat_degree f,  _ ⟩,
  intros a,
  simp only [mem_sdiff, mem_support_iff, ne.def, mem_singleton],
  split,
    { rw [and_imp],
      intros a_1 a_2,
      rwa erase_ne a_2, },
    { 
      intro,
      split,
        rwa erase_ne at a_1;
          { intro,
            subst a_2,
            apply a_1 erase_same, },
          { intro,
            subst a_2,
            apply a_1 erase_same, }, },
end

[bryangingechen]

Don't forget to add copyright headers and module docstrings to all new files.

[awainverse]

Seeing as we already have finsupp.erase used in the polynomial library, I'd like to be consistent with that, and use finsupp.erase to implement this function. I know you expressed some qualms about the computability, so I'd like to summon someone more knowledgeable than myself to judge this. My impression, though, was that in the polynomial library, we've kind of thrown all computability out the window, so we shouldn't worry.

[adomani]

Ok, I will wait a little bit longer to see if someone else chimes in. Otherwise, I will switch to noncomputable.

[jcommelin]

Hey @adomani, sorry for the delay... would you mind starting a new PR for each file in this PR (you can leave this one open for the big overview).

If file X depends on Y, then the PR that proposes X should also include file Y, and we can then treat it as an incremental PR.

Currently there are 4 files. I think it would be good to focus on the one that doesn't depend on others first. Then we can give detailed feedback on that.

[adomani]

@awainverse @jcommelin
All that is not yet in mathlib from this PR is the proof that reverse is a multiplicative monoid homomorphism. The PR #4598 contains a proof of this. I will therefore close this PR, if you agree!

Thank you for your help!

[adomani]

All that was contained in this PR has been merged through a couple of different PRs (#4527 and #4598).