isIntegral — Mathlib

English

If A is algebraic over K, then A is integral over K.

Русский

Если A над K алгебраическая, то A интегральна над K.

LaTeX

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

Lean4

/-- This used to be an `alias` of `Algebra.isAlgebraic_iff_isIntegral` but that would make
`Algebra.IsAlgebraic K A` an explicit parameter instead of instance implicit. -/
protected instance isIntegral [Algebra.IsAlgebraic K A] : Algebra.IsIntegral K A :=
  Algebra.isAlgebraic_iff_isIntegral.mp ‹_›

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