PolyChoose

Let $m, n$ be natural numbers. Prove that the polynomial $$\sum_{i = 0}^{m} {n + i \choose n} x^i$$ has at most one root (including multiplicities).

_Replace_ `sorry` _in the template below with your solution. Mathlib version used by the checker is v4.28.0_.

import Mathlib.Data.Fintype.BigOperators
import Mathlib.Order.Interval.Finset.Nat
import Mathlib.Data.Real.Basic
import Mathlib.Algebra.Polynomial.Roots

noncomputable
def P (m n : ℕ) : Polynomial ℝ :=
    ∑ i ∈ Finset.Icc 0 m, Polynomial.monomial i ((n + i).choose n)

theorem solution (m n : ℕ) : (P m n).roots.card ≤ 1 := sorry

Submit Solution

Login to submit a solution.

Recent Submissions