mem_nonzeroDivisors_of_coeff_mem — Mathlib

English

If the nth coefficient of a polynomial P lies in the nonzero divisors of R, then P itself lies in the zerodivisors of R[X].

Русский

Если коэффициент P при X^n является не нулевым делителем в R, то сам полином P принадлежит к нулевым делителям в R[X].

LaTeX

$$$ p \in R[X]^{0} \leftarrow\rightarrow p.coeff\ n \in R^{0} $$$

Lean4

theorem mem_nonzeroDivisors_of_coeff_mem {p : R[X]} (n : ℕ) (hp : p.coeff n ∈ R⁰) : p ∈ R[X]⁰ :=
  Polynomial.mem_nonZeroDivisors_iff.mpr fun r hr ↦ hp.2 _ (by simpa using congr(coeff $hr n))

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