IsAlgebraic — Mathlib

English

Let x ∈ L and p ∈ K[X] with aeval x p = 0 and coeff 0 ≠ 0. Then x⁻¹ equals negative of aeval x (divX p) divided by algebraMap K L (p.coeff 0).

Русский

Пусть x ∈ L и p ∈ K[X], aeval x p = 0, p(0) ≠ 0. Тогда x⁻¹ = − aeval x(divX p) / algebraMap_K L(p(0)).

LaTeX

$$$\\text{aeval}_x(p) = 0 \\to x^{-1} = -\\dfrac{\\text{aeval}_x(\\operatorname{divX} p)}{\\operatorname{algebraMap}(K,L)(p(0))}$$$

Lean4

/-- An element of an R-algebra is algebraic over R if it is a root of a nonzero polynomial
with coefficients in R. -/
@[stacks 09GC "Algebraic elements"]
def IsAlgebraic (x : A) : Prop :=
  ∃ p : R[X], p ≠ 0 ∧ aeval x p = 0

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