Lean Online Judge

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. The Mathlib version currently used is v4.26.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