English
Two polynomials f and g are coprime over a field K if and only if for every K-algebra A and every a ∈ A, aeval a f ≠ 0 or aeval a g ≠ 0.
Русский
Два полинома f и g над полем K приводят к взаимно простым, если и только если для каждого K-алгебры A и каждого элемента a ∈ A не выполняется одновременная равенство нулю aeval a f = 0 и aeval a g = 0.
LaTeX
$$$\\operatorname{IsCoprime}(f,g) \\iff \\forall A [\\text{CommRing }A][\\text{IsDomain }A][\\text{Algebra }K A](a:\\,A),\\ a\\operatorname{eval} f(a) \\neq 0 \\lor a\\operatorname{eval} g(a) \\neq 0$$$
Lean4
theorem isCoprime_iff_aeval_ne_zero (f g : K[X]) :
IsCoprime f g ↔ ∀ {A : Type v} [CommRing A] [IsDomain A] [Algebra K A] (a : A), aeval a f ≠ 0 ∨ aeval a g ≠ 0 :=
by
refine ⟨fun h => aeval_ne_zero_of_isCoprime h, fun h => isCoprime_of_dvd _ _ ?_ fun x hx _ => ?_⟩
· replace h := @h K _ _ _ 0
contrapose! h
rw [h.left, h.right, map_zero, and_self]
· rintro ⟨_, rfl⟩ ⟨_, rfl⟩
replace h := not_and_or.mpr <| h <| AdjoinRoot.root x.factor
simp only [AdjoinRoot.aeval_eq, AdjoinRoot.mk_eq_zero, dvd_mul_of_dvd_left <| factor_dvd_of_not_isUnit hx, true_and,
not_true] at h
