adjoin_of_disjoint — Mathlib

English

If x is algebraically independent over R and s, t are disjoint subsets of the index set, then the elements x_i with i in t are algebraically independent over the subalgebra adjoin_R(x''s).

Русский

Если x алгебраически независим над R и подмножества s, t несовпадают, то набор {x_i | i ∈ t} алгебраически независим над подалгеброй adjoin_R(x''s).

LaTeX

$$$\\mathrm{AlgebraicIndependent}_R x \\to \\mathrm{Disjoint}(s,t) \\to \\mathrm{AlgebraicIndependent}_{\\operatorname{adjoin}_R(x''s)} (x|_t)$$$

Lean4

theorem adjoin_of_disjoint {s t : Set ι} (h : Disjoint s t) :
    AlgebraicIndependent (adjoin R (x '' s)) fun i : t ↦ x i :=
  ((iff_adjoin_image s).mp hx).2.comp (inclusion _) (inclusion_injective h.subset_compl_left)

Похожие утверждения