algebraicIndependent_iff — Mathlib

English

Let x be algebraically independent over R. If S is an extension of R that is algebraic, then x is algebraically independent over S as well, and conversely; in other words, AlgebraicIndependent R x is equivalent to AlgebraicIndependent S x under algebraicity of R ⟶ S.

Русский

Пусть x алгебраически независимо над R. Если S является алгебраическим расширением R, то x алгебраически независимо над S, и наоборот; то есть AlgebraicIndependent R x эквивалентно AlgebraicIndependent S x при условии алгебраичности R ⟶ S.

LaTeX

$$$\\\\mathrm{AlgebraicIndependent}(R,x) \\\\iff \\\\mathrm{AlgebraicIndependent}(S,x)$$$

Lean4

protected theorem algebraicIndependent_iff [Algebra.IsAlgebraic R S] :
    AlgebraicIndependent R x ↔ AlgebraicIndependent S x :=
  ⟨(·.extendScalars _), (·.restrictScalars (FaithfulSMul.algebraMap_injective R S))⟩

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