algebraicIndependent_adjoin — Mathlib

English

If x is algebraically independent over R, then the embedding of x into adjoin R (range x) is algebraically independent.

Русский

Если x алгебраически независим над R, то копии x внутри подалгебры adjoin_R(range x) также алгебраически независимы над R.

LaTeX

$$$\\text{AlgebraicIndependent}_R x \\Rightarrow \\text{AlgebraicIndependent}_R( i \\mapsto ⟨x_i, \\subseteq(\\text{adjoin})⟩)$$$

Lean4

theorem algebraicIndependent_adjoin (hs : AlgebraicIndependent R x) :
    @AlgebraicIndependent ι R (adjoin R (range x)) (fun i : ι => ⟨x i, subset_adjoin (mem_range_self i)⟩) _ _ _ :=
  AlgebraicIndependent.of_comp (adjoin R (range x)).val hs

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