mem_nonZeroDivisors_of_trailingCoeff

English

If the trailing coefficient of p is a non-zero divisor in R, then p is a non-zero divisor in R[X].

Русский

Если концевой коэффициент p является ненулевым делителем в R, тогда p является ненулевым делителем в R[X].

LaTeX

$$$$ p_{\\text{trailingCoeff}} \\in \\operatorname{nonZeroDivisors}(R) \\Rightarrow p \\in \\operatorname{nonZeroDivisors}(R[X]). $$$$

Lean4

theorem mem_nonZeroDivisors_of_trailingCoeff {p : R[X]} (h : p.trailingCoeff ∈ R⁰) : p ∈ R[X]⁰ :=
  mem_nonzeroDivisors_of_coeff_mem _ h

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