English
If r is transcendental over R and f is transcendental over R, then aeval r f is transcendental over R.
Русский
Если r трансцендентен над R и f трансцендентен над R, то aeval r f трансцендентен над R.
LaTeX
$$$ \forall r : A,\ (H : Transcendental R r) \to \forall f : R[X],\ (hf : Transcendental R f) \to Transcendental R (Polynomial.aeval r f) $$$
Lean4
/-- If `r : A` and `f : R[X]` are transcendental over `R`, then `Polynomial.aeval r f` is also
transcendental over `R`. For the converse, see `Transcendental.of_aeval` and
`transcendental_aeval_iff`. -/
theorem aeval_of_transcendental {r : A} (H : Transcendental R r) {f : R[X]} (hf : Transcendental R f) :
Transcendental R (Polynomial.aeval r f) :=
by
rw [transcendental_iff] at H hf ⊢
intro p hp
exact hf _ (H _ (by rwa [← aeval_comp, comp_eq_aeval] at hp))
