English
If the images under aeval x of a family f are algebraically independent over R, then the family f itself is algebraically independent over R.
Русский
Если образы под aeval x для семейства f алгебраически независимы над R, то само семейство f алгебраически независимо над R.
LaTeX
$$$\\\\mathrm{AlgebraicIndependent}(R, (\\\\operatorname{aeval}_x)\\\\, f) \\\\Rightarrow \\\\mathrm{AlgebraicIndependent}(R, f)$$$
Lean4
/-- If `{f_i(x) | i : ι}` is algebraically independent over `R`, then
`{f_i : MvPolynomial ι R | i : ι}` is also algebraically independent over `R`.
In fact, the `x = {x_i : A | i : ι}` is also transcendental over `R` provided that `R`
is a field and `ι` is finite; the proof needs transcendence degree. -/
theorem of_aeval {f : ι → MvPolynomial ι R} (H : AlgebraicIndependent R fun i ↦ aeval x (f i)) :
AlgebraicIndependent R f := by
rw [algebraicIndependent_iff] at H ⊢
intro p hp
exact H p (by rw [← aeval_comp_bind₁, AlgHom.comp_apply, bind₁, hp, map_zero])
