isAlgebraic_iff_bot — Mathlib

English

If S is algebraic over R and S acts faithfully, then algebraicity over R of A is equivalent to algebraicity over R of S; the other direction is given by a tower construction.

Русский

Если S алгебраично над R и верно притязательное действие, то алгебраичность над R элемента A эквивалентна алгебраичности над R элемента S; обратное направление задаётся конструированием башни.

LaTeX

$$$[Algebra.IsAlgebraic S A] \\land [FaithfulSMul S A] \\Rightarrow (\\text{IsAlgebraic}_R A \\iff \\text{IsAlgebraic}_R S)$$$

Lean4

theorem isAlgebraic_iff_bot [Algebra.IsAlgebraic S A] [FaithfulSMul S A] :
    Algebra.IsAlgebraic R A ↔ Algebra.IsAlgebraic R S :=
  ⟨fun _ ↦ .tower_bot_of_injective (FaithfulSMul.algebraMap_injective S A), fun _ ↦ .trans R S A⟩

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