isAlgebraic_iff — Mathlib

English

For a tower of algebras with faithful scalar action and R→S algebraic, an element a ∈ A is algebraic over R if and only if it is algebraic over S.

Русский

Для башни алгебр с верным действием скаляров и при алгебраичности R→S элемент a ∈ A алгебраичен над R тогда и только тогда, когда он алгебраичен над S.

LaTeX

$$$\\IsAlgebraic_R A \\iff \\IsAlgebraic_S A$$$

Lean4

protected theorem isAlgebraic_iff [Algebra.IsAlgebraic R S] [FaithfulSMul R S] {a : A} :
    IsAlgebraic R a ↔ IsAlgebraic S a :=
  ⟨.extendScalars (FaithfulSMul.algebraMap_injective ..), .restrictScalars _⟩

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