ascPochhammer_eval_eq_zero_iff — Mathlib

English

Over an integral domain, the zeros of ascPochhammer occur exactly at −r with r = k for some k < n.

Русский

В интегральном домене нули ascPochhammer находятся и только при −r, где r = k и k < n.

LaTeX

$$$\text{IsDomain}(R)\;\Rightarrow\; (\ascPochhammer R\; n).eval(r)=0 \iff \exists k

Lean4

/-- Over an integral domain, the Pochhammer polynomial of degree `n` has roots *only* at
`0`, `-1`, ..., `-(n - 1)`. -/
@[simp]
theorem ascPochhammer_eval_eq_zero_iff [IsDomain R] (n : ℕ) (r : R) :
    (ascPochhammer R n).eval r = 0 ↔ ∃ k < n, k = -r :=
  by
  refine ⟨fun zero' ↦ ?_, fun hrn ↦ ?_⟩
  ·
    induction n with
    | zero => simp only [ascPochhammer_zero, Polynomial.eval_one, one_ne_zero] at zero'
    | succ n ih =>
      rw [ascPochhammer_succ_eval, mul_eq_zero] at zero'
      cases zero' with
      | inl h =>
        obtain ⟨rn, hrn, rrn⟩ := ih h
        exact ⟨rn, by cutsat, rrn⟩
      | inr h => exact ⟨n, lt_add_one n, eq_neg_of_add_eq_zero_right h⟩
  · obtain ⟨rn, hrn, rnn⟩ := hrn
    convert ascPochhammer_eval_neg_coe_nat_of_lt hrn
    simp [rnn]

Похожие утверждения