isAlgebraic_iff — Mathlib

English

Let R ⊆ S with S integral over R and the scalar action faithful. Then every element of A is algebraic over R iff it is algebraic over S.

Русский

Пусть R и S связаны так, что S целочисленно над R, и действие скаляра инъективно. Тогда каждый элемент A алгебраичен над R тогда и только тогда, когда он алгебраичен над S.

LaTeX

$$$[\text{IsIntegral}(R,S)] \land [\text{FaithfulSMul}(R,S)] \Rightarrow (IsAlgebraic(R,A) \iff IsAlgebraic(S,A)).$$$

Lean4

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

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