English
If x is algebraically independent over R and for every i the polynomial f_i is transcendental over R, then the family {Polynomial.aeval (x_i) (f_i)} is algebraically independent over R.
Русский
Если x алгебраически независим над R, и каждый f_i ∈ R[X] трансцендентен над R, то семейство {Polynomial.aeval (x_i) (f_i)} алгебраически независимо над R.
LaTeX
$$$\\mathrm{AlgebraicIndependent}_R x \\to \\forall i, \\mathrm{Transcendental}_R(f_i) \\Rightarrow \\mathrm{AlgebraicIndependent}_R\\bigl( i \\mapsto \\mathrm{Polynomial}.\\mathrm{aeval}(x_i) (f_i) \\bigr)$$$
Lean4
/-- If `{x_i : A | i : ι}` is algebraically independent over `R`, and for each `i`,
`f_i : R[X]` is transcendental over `R`, then `{f_i(x_i) | i : ι}` is also
algebraically independent over `R`. -/
theorem polynomial_aeval_of_transcendental (hx : AlgebraicIndependent R x) {f : ι → Polynomial R}
(hf : ∀ i, Transcendental R (f i)) : AlgebraicIndependent R fun i ↦ Polynomial.aeval (x i) (f i) :=
by
convert aeval_of_algebraicIndependent hx (algebraicIndependent_polynomial_aeval_X _ hf)
rw [← AlgHom.comp_apply]
congr 1; ext1; simp
