English
McCoy’s theorem: a polynomial P is not a zerodivisor if and only if there exists a nonzero a with a · P ≠ 0; equivalently, P ∉ nonZeroDivisors iff ∃ a ≠ 0 with a · P = 0.
Русский
Теорема Макоя: полином P не является нулевым делителем тогда и только тогда существует ненулевой a, такой что a · P ≠ 0; эквивалентно, P ∉ nonZeroDivisors ⇔ существует a ≠ 0 с a · P = 0.
LaTeX
$$$ P \notin \ R[X]^{0} \iff \exists a \neq 0,\ a \cdot P = 0 $$$
Lean4
/-- *McCoy theorem*: a polynomial `P : R[X]` is a zerodivisor if and only if there is `a : R`
such that `a ≠ 0` and `a • P = 0`. -/
theorem notMem_nonZeroDivisors_iff {P : R[X]} : P ∉ R[X]⁰ ↔ ∃ a : R, a ≠ 0 ∧ a • P = 0 :=
by
refine ⟨fun hP ↦ ?_, fun ⟨a, ha, h⟩ h1 ↦ ha <| C_eq_zero.1 <| (h1.2 _) <| smul_eq_C_mul a ▸ h⟩
by_contra! h
obtain ⟨Q, hQ⟩ := notMem_nonZeroDivisors_iff_right.1 hP
refine hQ.2 (eq_zero_of_mul_eq_zero_of_smul P (fun a ha ↦ ?_) Q (mul_comm P _ ▸ hQ.1))
contrapose! ha
exact h a ha
