integralClosure — Mathlib

English

Let a be transcendental over R in S; then a remains transcendental over R when viewed inside the integral closure of R in S.

Русский

Пусть a ∈ S транцендентно над R; тогда при рассмотрении a внутри интегрального замыкания R в S она остаётся транцендентной над R.

LaTeX

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

Lean4

protected theorem integralClosure : Transcendental (integralClosure R S) a :=
  ha.extendScalars_of_isIntegral _

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