isAlgebraic_adjoin_simple — Mathlib

English

If x is integral over K, then K⟮x⟯ is algebraic over K (repeat formulation).

Русский

Если x интегрально над K, то K⟮x⟯ алгебраическое над K (повтор формулировки).

LaTeX

$$IsIntegral K x → Algebra.IsAlgebraic K K⟮x⟯$$

Lean4

theorem isAlgebraic_adjoin_simple {x : L} (hx : IsIntegral K x) : Algebra.IsAlgebraic K K⟮x⟯ :=
  have := adjoin.finiteDimensional hx;
  Algebra.IsAlgebraic.of_finite K K⟮x⟯

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