subalgebraAlgebraicClosure — Mathlib

English

If a is transcendental over R, then a is transcendental over R when viewed in the algebraic closure of R in S.

Русский

Если a трансцендентно над R, то в алгебраическом замыкании R в S она остаётся трансцендентной над R.

LaTeX

$$$\\operatorname{Trans}_R(a) \\Rightarrow \\operatorname{Trans}_R(a) \\quad \\text{in } \\operatorname{Subalgebra.algebraicClosure}(R,S).$$$

Lean4

theorem subalgebraAlgebraicClosure [IsDomain R] : Transcendental (Subalgebra.algebraicClosure R S) a :=
  ha.extendScalars _

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