feat(data/polynomial/trinomial): Bundled trinomials

[tb65536]

This PR defines bundled trinomials. Working directly with specific polynomials (like X^n - X - 1) is really painful, since whenever you try to do something simple like checking that the polynomial is monic or computing its degree, you have to prove a bunch of trivial inequalities. Bundling solves this problem.

(this PR is part of the irreducibility saga)

---

• depends on: [Merged by Bors] - feat(data/polynomial/coeff): Alternate form of coeff_mul_X_pow #6424
• depends on: [Merged by Bors] - feat(data/polynomial/degree/trailing_degree): Trailing degree of multiplication by X^n #6425
• depends on: [Merged by Bors] - feat(data/polynomial/mirror): new file #6426
• depends on: feat(data/polynomial/mirror): define norm2 #6427

[github-actions]

This PR/issue depends on:

• [Merged by Bors] - feat(data/polynomial/coeff): Alternate form of coeff_mul_X_pow #6424
• [Merged by Bors] - feat(data/polynomial/degree/trailing_degree): Trailing degree of multiplication by X^n #6425
• [Merged by Bors] - feat(data/polynomial/mirror): new file #6426
• feat(data/polynomial/mirror): define norm2 #6427
  By Dependent Issues (🤖). Happy coding!

[semorrison]

I wonder if we should have binomial as well?

[tb65536]

I suppose so (although binomials aren't nearly as bad as trinomials, when working with them as polynomials).

[jcommelin]

I think almost all the lemmas in trinomial.lean should be simp-lemmas.

[eric-wieser]

Playing devil's advocate - would this definition be as easy to work with?

structure n_omial (R : Type*) (n : ℕ) [semiring R] :=
(coeffs : fin n → R)
(powers : fin n → ℕ)
(h_coeffs : ∀ i, coeffs i ≠ 0)
(h_powers : monotone powers) -- or `(list.of_fn powers).sorted (<))`, but that's likely harder to work with

abbreviation trinomial := n_omial 3

because it scales much better to working with "quadnomials" etc

[tb65536]

It would certainly be better than working with polynomials. I'll have to play around with this definition a bit to see whether it is nice to work with.

[tb65536]

I've defined to_polynomial and of_polynomial for n_omial, and proved that they are inverses. So far, things are working ok (and the amount of code is about the same). I'll continue to see how my proof ports over.

[tb65536]

@eric-wieser Here are my thoughts so far:

1. It seems possible to develop an API for n_omial, although some parts like n_omial.reverse' would be rather painful.
2. For the purposes of proving irreducibility of X^n - X -1, trinomial is much better than n_omial. The point of trinomial is that you can quickly figure what the nat_degree is or what the reverse' is (or other similar things). For n_omial, this is not the case. For example, the nat_degree of an n_omial is coeff (fin.mk n.pred (nat.pred_lt n_ne_zero), and the reverse' of an n_omial is also messy (the cleanest definition that I can think of involves passing to a list and invoking list.reverse).

[bryangingechen]

n_omials are sometimes called "fewnomials"; see also the chapter on "Bernstein's theorem and Fewnomials" in Sturmfels's book Solving systems of polynomial equations (though he never defines "fewnomial" formally, he just talks about polynomials with at most m distinct monomials).

[eric-wieser]

Ah, I see that it's not. Could you push the progress you made on that definition to a branch?

[tb65536]

There's a bunch of errors at the end, but here's what I have so far: https://github.com/leanprover-community/mathlib/compare/nomial

Feel free to play around with it.

[eric-wieser]

p.support.order_emb_of_fin can replace your definition of kth_power, and produces an order_embedding which already has lots of API.

[eric-wieser]

I've pushed to your branch with that change.

[eric-wieser]

It seems that this lemma is missing:

f : fin n ↪o ℕ
⊢ (finset.image ⇑f finset.univ).order_emb_of_fin _ = f