English
If x is algebraically independent, then extending by an a via an option index preserves independence if and only if a is transcendental over adjoin of range x.
Русский
Если x алгебраически независим, то расширение через опцию сохраняет независимость тогда и только тогда, когда a трансцендентно над.adjoin{R}(range x).
LaTeX
$$$\forall (hx : AlgebraicIndependent R x) (a : A),\ AlgebraicIndependent R (fun o : Option ι \mapsto o.elim a x) \\iff Transcendental (adjoin R (range x)) a$$
Lean4
theorem option_iff_transcendental (hx : AlgebraicIndependent R x) (a : A) :
AlgebraicIndependent R (fun o : Option ι ↦ o.elim a x) ↔ Transcendental (adjoin R (range x)) a :=
by
rw [algebraicIndependent_iff_injective_aeval, transcendental_iff_injective, ← AlgHom.coe_toRingHom, ←
hx.aeval_comp_mvPolynomialOptionEquivPolynomialAdjoin, RingHom.coe_comp]
exact Injective.of_comp_iff' (Polynomial.aeval a) (mvPolynomialOptionEquivPolynomialAdjoin hx).bijective
