tower_top — Mathlib

English

If A is algebraic over K, then A is algebraic over L when L is an extension of K.

Русский

Если A алгебраичен над K, то A алгебраичен над L, если L является расширением K.

LaTeX

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

Lean4

/-- If `x` is algebraic over `K`, then `x` is algebraic over `L` when `L` is an extension of `K` -/
@[stacks 09GF "part one"]
theorem tower_top {x : A} (A_alg : IsAlgebraic K x) : IsAlgebraic L x :=
  A_alg.extendScalars (algebraMap K L).injective

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