tower_bot — Mathlib

English

If A is an algebraic algebra over K, then A is algebraic over L for any extension L of K.

Русский

Если A — алгебра над K и K ⊆ L, то A алгебраичен над L.

LaTeX

$$$[\mathrm{Algebra.IsAlgebraic}\ K\ A] \Rightarrow \mathrm{Algebra.IsAlgebraic}\ L\ A$$$

Lean4

theorem tower_bot (K L A : Type*) [CommRing K] [Field L] [Ring A] [Algebra K L] [Algebra L A] [Algebra K A]
    [IsScalarTower K L A] [Nontrivial A] [Algebra.IsAlgebraic K A] : Algebra.IsAlgebraic K L :=
  tower_bot_of_injective (algebraMap L A).injective

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