isAlgebraic_def — Mathlib

English

An element x of an R-algebra A is algebraic over R if there exists a nonzero polynomial p ∈ R[X] with aeval x p = 0.

Русский

Элемент x алгебраичен над R если существует ненулевой многочлен p ∈ R[X], такой что aeval x p = 0.

LaTeX

$$$\\exists p\\in R[X], p\\neq 0 \\land \\operatorname{aeval}_{x} p = 0$$$

Lean4

theorem isAlgebraic_def : Algebra.IsAlgebraic R A ↔ ∀ x : A, IsAlgebraic R x :=
  ⟨fun ⟨h⟩ ↦ h, fun h ↦ ⟨h⟩⟩

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