IsIntegralElem — Mathlib

English

An element x of A is said to be integral over R with respect to a map f : R →+* A if there exists a monic polynomial p ∈ R[X] such that eval₂ f x p = 0.

Русский

Элемент x в A называется интегральным над R относительно отображения f, если существует моническое многочлен p ∈ R[X], такой что eval₂ f x p = 0.

LaTeX

$$$\\exists p : R[X],\\ Monic\\ p \\wedge eval\\_2 f x p = 0$$$

Lean4

/-- An element `x` of `A` is said to be integral over `R` with respect to `f`
if it is a root of a monic polynomial `p : R[X]` evaluated under `f` -/
def IsIntegralElem (f : R →+* A) (x : A) :=
  ∃ p : R[X], Monic p ∧ eval₂ f x p = 0

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