mem_nonZeroDivisors_iff — Mathlib

English

For a polynomial P, P lies in the zerodivisors of R[X] if and only if for every a ∈ R, a · P = 0 implies a = 0.

Русский

Для полинома P верно: P принадлежит нулевым делителям R[X] тогда и только тогда, когда для каждого a ∈ R верно a · P = 0 ⇒ a = 0.

LaTeX

$$$ P \in R[X]^{0} \iff \forall a \in R,\ a \cdot P = 0 \Rightarrow a = 0 $$$

Lean4

protected theorem mem_nonZeroDivisors_iff {P : R[X]} : P ∈ R[X]⁰ ↔ ∀ a : R, a • P = 0 → a = 0 := by
  simpa [not_imp_not] using (notMem_nonZeroDivisors_iff (P := P)).not

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