IsIntegral — Mathlib

English

An element x of A is integral over R if it is integral with respect to the canonical algebra map from R to A.

Русский

Элемент x в A интегральный над R, если он интегрален по каноническому отображению R в A.

LaTeX

$$$\\text{IsIntegral}(x) := (\\text{algebraMap } R A).IsIntegralElem(x)$$$

Lean4

/-- An element `x` of an algebra `A` over a commutative ring `R` is said to be *integral*,
if it is a root of some monic polynomial `p : R[X]`.
Equivalently, the element is integral over `R` with respect to the induced `algebraMap` -/
def IsIntegral (x : A) : Prop :=
  (algebraMap R A).IsIntegralElem x

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