IsIntegral — Mathlib

English

An element x of an algebra A over R is integral over R if it is a root of some monic polynomial with coefficients in R via the canonical map.

Русский

Элемент x алгебры A над R интегральный над R, если он является корнем некоторого монического многочлена с коэффициентами в R через каноническое отображение.

LaTeX

$$$\\text{IsIntegral}(x) \\iff \\exists p \\in R[X], Monic(p) \\wedge eval\\_2 (algebraMap\\ R A) x p = 0$$$

Lean4

/-- A ring homomorphism `f : R →+* A` is said to be integral
if every element `A` is integral with respect to the map `f` -/
@[algebraize Algebra.IsIntegral.mk, stacks 00GI "(2)"]
def IsIntegral (f : R →+* A) :=
  ∀ x : A, f.IsIntegralElem x

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