English
Over an algebraically closed field K, two polynomials p, q ∈ k[X] are coprime if and only if for every a ∈ K, at least one of p(a) or q(a) is nonzero after aevaluation.
Русский
Над полем K, если K алгебраически замкнутое, то ∀p, q ∈ k[X] верно: p и q coprime тогда и только тогда, когда для каждого a ∈ K хотя бы одно из p(a), q(a) не равно нулю.
LaTeX
$$$\forall (k : Type u) [\mathrm{Field}\;k] (K : Type v) [\mathrm{Field}\;K] [IsAlgClosed K] [Algebra k K] (p q : k[X]), IsCoprime p q \leftrightarrow \forall a : K, aeval a p \neq 0 \lor aeval a q \neq 0$$$
Lean4
theorem isCoprime_iff_aeval_ne_zero_of_isAlgClosed (K : Type v) [Field K] [IsAlgClosed K] [Algebra k K] (p q : k[X]) :
IsCoprime p q ↔ ∀ a : K, aeval a p ≠ 0 ∨ aeval a q ≠ 0 :=
by
refine ⟨fun h => aeval_ne_zero_of_isCoprime h, fun h => isCoprime_of_dvd _ _ ?_ fun x hu h0 => ?_⟩
· replace h := h 0
contrapose! h
rw [h.left, h.right, map_zero, and_self]
· rintro ⟨_, rfl⟩ ⟨_, rfl⟩
obtain ⟨a, ha : _ = _⟩ :=
IsAlgClosed.exists_root (x.map <| algebraMap k K) <| by
simpa only [degree_map] using (ne_of_lt <| degree_pos_of_ne_zero_of_nonunit h0 hu).symm
exact not_and_or.mpr (h a) (by simp_rw [map_mul, ← eval_map_algebraMap, ha, zero_mul, true_and])
