English
An element x is transcendental over R iff for every polynomial p with coefficients in R, aeval x p = 0 implies p = 0.
Русский
Элемент x трансцендентен над R тогда и только тогда, когда для любого многочлена p с коэффициентами в R, если aeval x p = 0, то p = 0.
LaTeX
$$$\\text{Transcendental}(R,x) \\iff \\forall p \\in R[X], \\; \\operatorname{aeval}_{x} p = 0 \\Rightarrow p = 0$$$
Lean4
/-- An element `x` is transcendental over `R` if and only if for any polynomial `p`,
`Polynomial.aeval x p = 0` implies `p = 0`. This is similar to `algebraicIndependent_iff`. -/
theorem transcendental_iff {x : A} : Transcendental R x ↔ ∀ p : R[X], aeval x p = 0 → p = 0 :=
by
rw [Transcendental, IsAlgebraic, not_exists]
congr! 1; tauto
