Working with polynomials

Stream: Is there code for X?

[Frédéric Dupuis]

This is the first time I'm trying to use polynomials in Lean, and this is proving to be more of a struggle than I anticipated. What I'm trying to do is very simple: I have a v : Fin n → R that I would like to consider as the coefficients of a polynomial. Then, all I want to say is that it has at most n-1 zeros if v ≠ 0. My first attempt was just something like this:

open scoped Polynomial in
noncomputable def toPoly (v : Fin n → R) : R[X] :=
  ∑ i, Polynomial.C (v i) * Polynomial.X ^ (i : ℕ)

but then showing that this is nonzero if v ≠ 0 is not direct. So then I tried going the finsupp route, and ended up writing this:

def Polynomial.ofCoeffs (c : Fin n → R) : Polynomial R where
  toFinsupp := { toFun := fun i => if h : i < n then c ⟨i, h⟩ else 0
                 support := (Finset.range n).filter (fun i => if h : i < n then c ⟨i, h⟩ ≠ 0 else False)
                 mem_support_toFun := fun i => by
                  refine ⟨fun h => ?_, fun h => ?_⟩
                  · rw [Finset.mem_filter] at h
                    by_cases hi : i < n
                    case pos =>
                      simp only [mem_range, hi, ne_eq, dite_true, true_and] at *
                      exact h
                    case neg => simp [hi] at *
                  · rw [Finset.mem_filter]
                    by_cases hi : i < n
                    case pos => simp [hi] at *; exact h
                    case neg => simp [hi] at * }

But surely I'm overcomplicating things here. Is there a straightforward way to do what I want?

[Ruben Van de Velde]

Going through Finsupp sounds like a pain. Maybe \smul is easier than C (v i) *?

[Frédéric Dupuis]

Well, the problem with the sum is that the terms of the sum "could" cancel out.

[Kevin Buzzard]

Note that $x^2-1$ has four zeros in $\Z/8\Z$.

[Frédéric Dupuis]

Let's say R is a field.

[Frédéric Dupuis]

(I should probably rename it to something more fieldlike in my code.)

[Ruben Van de Velde]

import Mathlib

variable (n : ℕ) (R : Type*) [Field R] (v : Fin n → R)

open scoped Polynomial BigOperators in
noncomputable def toPoly : R[X] :=
  ∑ i, v i • Polynomial.X ^ (i : ℕ)

example (h : v ≠ 0) : toPoly n R v ≠ 0 := by
  contrapose! h
  ext i
  simp only [Pi.zero_apply]
  trans (toPoly n R v).coeff i
  · simp only [toPoly, Polynomial.finset_sum_coeff, Polynomial.coeff_smul, Polynomial.coeff_X_pow,
      smul_eq_mul, mul_ite, mul_one, mul_zero]
    rw [@Finset.sum_ite]
    simp only [Finset.sum_const_zero, add_zero]
    simp_rw [Fin.val_inj]
    rw [Finset.filter_eq]
    simp only [Finset.mem_univ, ite_true, Finset.sum_singleton]
  · rw [h]
    simp only [Polynomial.coeff_zero]

[Kevin Buzzard]

It's true for integral domains

[Yakov Pechersky]

mathlib#15476:

def of_list : polynomial R :=
of_finsupp l.to_finsupp

example {n : Nat) (v : Fin n → R) : polynomial R := of_list (.ofFn v)

[Frédéric Dupuis]

Yakov Pechersky said:

mathlib#15476:

def of_list : polynomial R :=
of_finsupp l.to_finsupp

example {n : Nat) (v : Fin n → R) : polynomial R := of_list (.ofFn v)

This is what I was hoping to find somewhere! Are you planning to port that PR?

[Frédéric Dupuis]

In the meantime I'll use @Ruben Van de Velde's solution -- thanks!

[Yakov Pechersky]

I haven't had any mathlib time in months, so I've unfortunately had to let it linger. I hope that porting would be straightforward, the prereqs are merged iirc.

[Ruben Van de Velde]

I'm taking a look; unfortunately !3#18182 broke it

[Ruben Van de Velde]

I managed to get it to compile at https://github.com/leanprover-community/mathlib4/pull/9973 by removing all the decidability arguments. Still 27 deprecation warnings around List.nthLe. I'm not planning any further work on it

[Yakov Pechersky]

The hope of the decidability arguments was to have a "computable" list-based way of generating polynomials. Since I can't help currently, it's not my place to say that that is a requirement. Perhaps when I have time again, I'll be able to build in the computability aspect.

[Kim Morrison]

My PR std4#556 introducing OrderedAssocList is intended initially for internal use by omega, but could potentially be useful for computable polynomials. (Although RBMap is probably suitable too.)