English
If Polynomial.aeval r f is transcendental over R, then f is transcendental over R.
Русский
Если Polynomial.aeval r f трансцендентен над R, то f трансцендентен над R.
LaTeX
$$$ {r : A} \{f : R[X]\} (H : Transcendental R (Polynomial.aeval r f)) : Transcendental R f $$$
Lean4
/-- If `Polynomial.aeval r f` is transcendental over `R`, then `f : R[X]` is also
transcendental over `R`. In fact, the `r` is also transcendental over `R` provided that `R`
is a field (see `transcendental_aeval_iff`). -/
theorem of_aeval {r : A} {f : R[X]} (H : Transcendental R (Polynomial.aeval r f)) : Transcendental R f :=
by
rw [transcendental_iff] at H ⊢
intro p hp
exact H p (by rw [← aeval_comp, comp_eq_aeval, hp, map_zero])
