mem_nonZeroDivisors_of_leadingCoeff

English

If the leading 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{leadingCoeff}} \\in \\operatorname{nonZeroDivisors}(R) \\Rightarrow p \\in \\operatorname{nonZeroDivisors}(R[X]). $$$$

Lean4

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

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