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.29.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