# Zulip Chat Archive

## Stream: maths

### Topic: Constructing Polynomials

#### Thomas Browning (Oct 25 2020 at 20:37):

If I have `f : (↑(finset.range n) : set ℕ) → F`

, what's the best way to turn this into a polynomial (where `f`

is giving the coefficients of the polynomial)? It seems like a polynomial is secretly a finsupp, but turning `f`

into a finsupp seems a bit painful (since some of the coefficients could be zero).

#### Reid Barton (Oct 25 2020 at 20:38):

Probably something involving a suitable sum of `f i * X^i`

#### Kevin Buzzard (Oct 25 2020 at 20:39):

And your next question is how to prove that the coefficient of $X^i$ is $f(i)$, right?

#### Johan Commelin (Oct 25 2020 at 20:44):

```
/-- `on_finset s f hf` is the finsupp function representing `f` restricted to the finset `s`.
The function needs to be `0` outside of `s`. Use this when the set needs to be filtered anyways,
otherwise a better set representation is often available. -/
def on_finset (s : finset α) (f : α → M) (hf : ∀a, f a ≠ 0 → a ∈ s) : α →₀ M :=
⟨s.filter (λa, f a ≠ 0), f, by simpa⟩
```

#### Johan Commelin (Oct 25 2020 at 20:44):

L298 of `data.finsupp.basic`

#### Reid Barton (Oct 25 2020 at 20:45):

and now your next question is how to show that when you evaluate it at `x : F`

it agrees with the sum `f i * x^i`

, right?

#### Thomas Browning (Oct 25 2020 at 20:46):

@Johan Commelin I saw that, but wouldn't I need to extend f to all of the natural numbers?

#### Thomas Browning (Oct 25 2020 at 20:47):

@Reid Barton Actually it's just Kevin's question that I need

#### Thomas Browning (Oct 25 2020 at 20:47):

At the end, I just need to know that it's a polynomial of degree less than n whose coefficients agree with f

#### Reid Barton (Oct 25 2020 at 20:48):

ah, lucky. But in general, using this `on_finset`

directly would be breaking the abstraction that `polynomial`

provides (or pretends to provide)

#### Thomas Browning (Oct 25 2020 at 23:49):

For reference, I ended up going with the `finsupp.on_finset`

approach, by first extending `f`

to `ℕ`

by `let g : ℕ → F := λ k, dite (k < n) (λ h, f ⟨k, finset.mem_coe.mpr (finset.mem_range.mpr h)⟩) (λ h, 0),`

#### Thomas Browning (Oct 25 2020 at 23:50):

it ended up being fine, albeit rather longwinded

Last updated: May 11 2021 at 17:39 UTC