English
Let r ∈ A and f ∈ K[X]. Then Polynomial.aeval r f is transcendental over K iff r and f are both transcendental over K.
Русский
Пусть r ∈ A и f ∈ K[X]. Тогда ∀ транcцендентность над K: aeval r f транcендентно тогда и только тогда, когда r и f оба транcцендентны над K.
LaTeX
$$$Transcendental\ K\ (Polynomial.aeval\ r\ f) \iff (Transcendental\ K\ r \wedge Transcendental\ K\ f)$$$
Lean4
/-- If `K` is a field, `r : A` and `f : K[X]`, then `Polynomial.aeval r f` is
transcendental over `K` if and only if `r` and `f` are both transcendental over `K`.
See also `Transcendental.aeval_of_transcendental` and `Transcendental.of_aeval`. -/
@[simp]
theorem transcendental_aeval_iff {r : A} {f : K[X]} :
Transcendental K (Polynomial.aeval r f) ↔ Transcendental K r ∧ Transcendental K f :=
by
refine ⟨fun h ↦ ⟨?_, h.of_aeval⟩, fun ⟨h1, h2⟩ ↦ h1.aeval_of_transcendental h2⟩
rw [Transcendental] at h ⊢
contrapose! h
rw [isAlgebraic_iff_isIntegral] at h ⊢
exact .of_mem_of_fg _ h.fg_adjoin_singleton _ (aeval_mem_adjoin_singleton _ _)
