isAlgebraic_iff_isIntegral — Mathlib

English

In a K-algebra A, A is algebraic over K if and only if A is integral over K.

Русский

В K-алгебре A A алгебраическая над K тогда и только тогда является интегральной над K.

LaTeX

$$$Algebra.IsAlgebraic\ K\ A \iff Algebra.IsIntegral\ K\ A$$$

Lean4

protected theorem isAlgebraic_iff_isIntegral : Algebra.IsAlgebraic K A ↔ Algebra.IsIntegral K A := by
  rw [Algebra.isAlgebraic_def, Algebra.isIntegral_def, forall_congr' fun _ ↦ isAlgebraic_iff_isIntegral]

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