English
Let x_i (i ∈ I) be algebraically independent over R in A, and let y_j (j ∈ J) be algebraically independent over the subalgebra adjoin_R(range x). Then the combined family obtained by interleaving y and x, i.e. Sum.elim y x, is algebraically independent over R.
Русский
Пусть x_i (i ∈ I) алгебраически независимы над R в A, и пусть y_j (j ∈ J) алгебраически независимы над подалгеброй adjoin_R(range x). Тогда объединение через суммирование, то есть Sum.elim y x, алгебраически независимо над R.
LaTeX
$$$\\mathrm{AlgebraicIndependent}_R x \\to \\mathrm{AlgebraicIndependent}_{\\operatorname{adjoin}_R(\\operatorname{range} x)} y \\to \\mathrm{AlgebraicIndependent}_R(\\mathrm{Sum\\_elim}\\; y\\; x)$$$
Lean4
theorem sumElim {ι'} {y : ι' → A} (hy : AlgebraicIndependent (adjoin R (range x)) y) :
AlgebraicIndependent R (Sum.elim y x) :=
sumElim_iff.mpr ⟨hx, hy⟩
