English
If f is a family of polynomials algebraically independent over R and x is algebraically independent over R, then the image under aeval x of f is algebraically independent over R.
Русский
Если f — множество полиномов алгебраически независимых над R, и x алгебраически независимо над R, то образы f под aeval x также алгебраически независимы над R.
LaTeX
$$$\\\\mathrm{AlgebraicIndependent}(R,x) \\Rightarrow \\\\mathrm{AlgebraicIndependent}(R, f) \\\\Rightarrow \\\\mathrm{AlgebraicIndependent}(R) (\\\\operatorname{aeval}_x f)$$$
Lean4
/-- If `x = {x_i : A | i : ι}` and `f = {f_i : MvPolynomial ι R | i : ι}` are algebraically
independent over `R`, then `{f_i(x) | i : ι}` is also algebraically independent over `R`.
For the partial converse, see `AlgebraicIndependent.of_aeval`. -/
theorem aeval_of_algebraicIndependent {f : ι → MvPolynomial ι R} (hf : AlgebraicIndependent R f) :
AlgebraicIndependent R fun i ↦ aeval x (f i) :=
by
rw [algebraicIndependent_iff] at hx hf ⊢
intro p hp
exact hf _ (hx _ (by rwa [← aeval_comp_bind₁, AlgHom.comp_apply] at hp))
