transcendental_iff — Mathlib

English

If [Algebra.IsAlgebraic R S], then Transcendental R(a) is equivalent to Transcendental S(a).

Русский

Если расширение R → S алгебраическое, тогда трансцендентность над R равна трансцендентности над S для элемента a.

LaTeX

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

Lean4

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

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