English
If s is finite and the restriction of x to s is algebraically independent, and a certain transcendence condition holds for all finite t ⊆ ι, then x is algebraically independent.
Русский
Если s конечно и ограничение x на s алгебраически независимо, и для всех конечных t ⊆ ι выполняется требование трансцендентности, тогда x алгебраически независимо.
LaTeX
$$$\forall s:\ Set ι,\ AlgebraicIndependent R (fun i : s \mapsto x i)\to (\forall t : Set ι, t.Finite \to AlgebraicIndependent R (fun i : t \mapsto x i) \to \forall i \notin s, i \notin t, Transcendental (adjoin R (x '' t)) (x i)) \to AlgebraicIndependent R x$$
Lean4
protected theorem insert {s : Set ι} {i : ι} (hs : AlgebraicIndepOn R x s)
(hi : Transcendental (adjoin R (x '' s)) (x i)) : AlgebraicIndepOn R x (insert i s) :=
by
nontriviality R
have := hs.algebraMap_injective.nontrivial
exact
(insert_iff fun h ↦ hi <| isAlgebraic_algebraMap (⟨_, subset_adjoin ⟨i, h, rfl⟩⟩ : adjoin R (x '' s))).mpr ⟨hs, hi⟩
