English
If x is algebraically independent and f is an injective algebra homomorphism A → A', then AlgebraicIndependent R x is equivalent to AlgebraicIndependent R (f ∘ x).
Русский
Если x алгебраически независимо и f — инъективное алгебраическое гомоморфизм A → A', то AlgebraicIndependent R x эквивалентно AlgebraicIndependent R (f ∘ x).
LaTeX
$$$\\\\mathrm{AlgebraicIndependent}(R,x) \\\\Rightarrow \\\\mathrm{AlgebraicIndependent}(R,f\\\\circ x)$ и наоборот; точнее: $\\\\mathrm{AlgebraicIndependent}(R,x) \iff \\\\mathrm{AlgebraicIndependent}(R,f\\\\circ x)$$$
Lean4
theorem linearIndependent : LinearIndependent R x :=
by
rw [linearIndependent_iff_injective_finsuppLinearCombination]
have : Finsupp.linearCombination R x = (MvPolynomial.aeval x).toLinearMap.comp (Finsupp.linearCombination R X) :=
by
ext
simp
rw [this]
refine (algebraicIndependent_iff_injective_aeval.mp hx).comp ?_
rw [← linearIndependent_iff_injective_finsuppLinearCombination]
exact linearIndependent_X _ _
