Factoring zero roots

Stream: Is there code for X?

[Yaël Dillies]

Is there a way to write a polynomial P as X ^ m * Q where the smallest coefficient of Q is nonzero that's well-integrated with coeff?

[Johan Commelin]

cc @Damiano Testa

[Yaël Dillies]

To un #xy, I just want to show that if the least nonzero coefficients of P and Q are positive, then the least coefficient of P * Q is as well. If it were the greatest, I could use leading_coeff and all would be well, but we don't seem to have something like least_coeff?

[Alex J. Best]

docs#polynomial.trailing_coeff

[Yaël Dillies]

Aaah trailing! I knew it had to be somewhere :smiley:

[Damiano Testa]

Yes, trailing coeff would work. There might be trailing_coeff_mul as well. I am not sure if there is a version with just the bounds (the analogue of docs#polynomial.nat_degree_mul_le.

[Damiano Testa]

Let's try: docs#polynomial.le_trailing_degree_mul.

It works!!! :octopus:

[Damiano Testa]

As for your initial question, I know that there is docs#multiplicity, I thought that it would have been useful, but so far I have never used it.

[Yaël Dillies]

I actually only need trailing_coeff_mul! So I now have a complete proof that floors and ceils are not preserved under ordered ring homomorphisms.

[Yaël Dillies]

That is, life is proven sad.

[Damiano Testa]

Is this a goals accomplished or goals not accomplished kind of thing?

[Yaël Dillies]

It's a "I have a new pathology to put in counterexamples" kind of thing.

[Damiano Testa]

I love counterexamples: if you play your cards right, you always either get a theorem or counterexample!

[Yaël Dillies]

Okay so intuitively floors and ceils should be preserved by f an ordered ring homs because:

• f preserves the copy of the naturals/integers because it's a ring hom.
• f preserves what's between n and n + 1 because it's monotone.

[Yaël Dillies]

At this point, I was quite happy with the proof and PRed #16025. But I couldn't get the Lean proof.

[Yaël Dillies]

And this was because that "between" doesn't have to be strict. Potentially something whose floor was n could get mapped to n + 1, and this has floor n + 1, not n.

[Yaël Dillies]

So what would be a counterexample? Not ℚ, ℝ or anything like that, because you can use archimedeanness to ensure that nothing < n + 1 gets mapped to n + 1. So you need infinitesimals.

[Yaël Dillies]

Hence I took ℤ[ε] where ε is an infinitesimal. I could inherit the ring structure from ℤ[X], and the ordered add group structure from ℕ →ₗ ℤ thanks to docs#pi.lex.ordered_add_comm_group.

[Yaël Dillies]

Now the pathological hom is taking the zeroth coefficient. That works because ⌊-ε⌋ = -1 but ⌊coeff (-ε) 0⌋ = ⌊0⌋ = 0.

[Damiano Testa]

This reminds me of another counterexample in the folder of a canonically_ordered something for which multiplication by 2 is not injective (if I remember correctly) and you get two incomparable elements a b such that 2 * a = 2 * b.