Construct a polynomial out of a vector

Stream: mathlib4

[Fabrizio Barroero]

In Diophantine approximation it is very important to jump between polynomials of bounded degree and the vectors of their coefficients. I could not find anything in Mathlib so I defined

noncomputable def Polynomial.ofFinToSemiring (n : ℕ) : (Fin (n + 1) → R) →+ R[X] where
  toFun v := ⟨let f : ℕ → R := fun i => if h : i < n + 1 then v ⟨i, h⟩ else 0
  {
    toFun := f,
    support := (Set.Finite.subset (t := f.support) (Finset.finite_toSet (Finset.range (n + 1)))
        (by simp_all [f])).toFinset,
    mem_support_toFun := by simp
  }⟩
  map_add' x y := by
    ext m
    simp only [Pi.add_apply, coeff_ofFinsupp, Finsupp.coe_mk, coeff_add]
    split; all_goals simp
  map_zero' := by simp; rfl

An alternative would be

noncomputable def Polynomial.ofFinToSemiring (n : ℕ) := fun f : Fin (n + 1) → R ↦ ∑ i in Finset.range (n + 1),
  Polynomial.monomial i (f i)

but I like the first more and moreover with the first definition the theorem

theorem Polynomial.of_fin_to_semiring_def {n : ℕ} (v : Fin (n + 1) → R) : (ofFinToSemiring n) v =
    ∑ i in Finset.range (n + 1), Polynomial.monomial i (v i)

has a pretty simple proof.

My question is: is the name ofFinToSemiring appropriate or should I choose ofVector? Or there are better names?
Also, am I right in preferring the first def?
Finally, I would like to add this to Mathlib. Any reason against?

[Eric Wieser]

Are you aware of docs#List.toFinsupp ?

[Eric Wieser]

(cc its author, @Yakov Pechersky )

[Eric Wieser]

Also worth noting that you almost certainly want ∑ i : Fin n, monomial i (v i) not ∑ i in Finset.range (n + 1), monomial i (v i), as the v i in the latter means v (i % n) which is going to be annoying.

[Yakov Pechersky]

I had a mathlib3 PRs on using this for polynomials:
https://github.com/leanprover-community/mathlib3/pull/15476
https://github.com/leanprover-community/mathlib3/pull/15477

one of which is partially ported as a mathlib4 pr
https://github.com/leanprover-community/mathlib4/pull/9973

[Yakov Pechersky]

So, one can have a fully "computable" function from Fin n -> R to R[X] using docs#List.ofFn and the above.

[Eric Wieser]

Well, with DecidableEq R, which is a bit silly; but I guess that's a different problem (solved by moving to DFinsupp...)

[Yakov Pechersky]

In fact, most lemmas should be proven about the list based construction (that it has a particular support, that the degree is lt, that it is injective)

[Yakov Pechersky]

A somewhat less strong Decidable:

DecidablePred (fun (i : ℕ), List.getD 0 l i ≠ 0)

[Yakov Pechersky]

But yes, we always come back to the DFinsupp issue, the D stands for dream

[Yakov Pechersky]

I think even with DecidableEq R, it's still worthwhile, since often one cares about polynomials with natural, integer, or rational coefficients

[Yakov Pechersky]

and one can lift that into your R of choice, either via aeval or map

[Fabrizio Barroero]

Thanks for the messages!
I was not aware of  docs#List.toFinsupp nor of docs#List.ofFn.
I can use them to define my desired function adding DecidableEq R or, as done in #9973, with

open scoped Classical
noncomputable section

While for most applications one needs R to be the integers or the rationals, I can think of some where R is a number field or its ring of integers and I guess there we do not have DecidableEq R.

[Kevin Buzzard]

The rule of thumb is: if the statement won't compile without the assumption, add [DecidableEq R] to the statement, but if a proof won't work without it then use classical in the proof. And yes you're right, DecidableEq won't be automatic for a random ring of integers of a random number field (I am not entirely sure about whether one could prove such an instance without any assumptions)

[Fabrizio Barroero]

In #23080 I add Polynomial.ofFn and prove some APIs. It would be great if someone could have look.