subalgebraAlgebraicClosure — Mathlib

English

Algebraic independence is preserved when passing to the algebraic closure of the base ring.

Русский

Независимость сохраняется при переходе к алгебраическому замыканию базы.

LaTeX

$$$$ hx \text{ extends scalars to algebraicClosure } R A: \ AlgebraicIndependent (algebraicClosure R A) x. $$$$

Lean4

theorem subalgebraAlgebraicClosure [IsDomain R] [NoZeroDivisors A] :
    AlgebraicIndependent (Subalgebra.algebraicClosure R A) x :=
  hx.extendScalars _

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