English
Same as sumElim_of_tower: x is algebraically independent over R, range x sits in range(algebraMap S A), y is algebraically independent over S, hence Sum.elim y x is algebraically independent over R.
Русский
То же, что и предыдущая: x алгебраически независим над R, диапазон x лежит в образе алгебра-map S→A, y алгебраически независим над S, значит Sum.elim y x алгебраически независим над R.
LaTeX
$$$\\mathrm{AlgebraicIndependent}_R x \\to (\\operatorname{range} x \\subseteq \\operatorname{range}(\\mathrm{algebraMap}\\,S\\,A)) \\to \\mathrm{AlgebraicIndependent}_S y \\to \\mathrm{AlgebraicIndependent}_R(\\mathrm{Sum\\_elim}\\; y\\; x)$$$
Lean4
theorem transcendental_adjoin {s : Set ι} {i : ι} (hi : i ∉ s) : Transcendental (adjoin R (x '' s)) (x i) :=
by
convert ← hx.adjoin_of_disjoint (Set.disjoint_singleton_right.mpr hi)
rw [algebraicIndependent_singleton_iff ⟨i, rfl⟩]
