transcendental_iff — Mathlib

English

Let R ⊆ S be an integral extension. Then for any a in A, Transcendental_R(a) is equivalent to Transcendental_S(a).

Русский

Пусть R является подкольцом S и S образует интегральное расширение; тогда для любого a ∈ A выполняется эквивалентность: трансцендентность над R равна трансцендентности над S.

LaTeX

$$$\\operatorname{Trans}_R(a) \\iff \\operatorname{Trans}_S(a).$$$

Lean4

protected theorem transcendental_iff [Algebra.IsIntegral R S] : Transcendental R a ↔ Transcendental S a :=
  ⟨(·.extendScalars_of_isIntegral _), (·.restrictScalars (FaithfulSMul.algebraMap_injective R S))⟩

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