isAlgebraic_root — Mathlib

English

If f ≠ 0, then the root h.root is algebraic over R; equivalently there exists a nonzero polynomial over R vanishing at h.root.

Русский

Если f ≠ 0, то корень h.root алгебраичен над R; эквивалентно существуют полином над R не равно нулю, так что он обнуляется в h.root.

LaTeX

$$$ \exists p \in R[X], p \neq 0 \wedge p(h.root) = 0 $$$

Lean4

theorem isAlgebraic_root (hf : f ≠ 0) : IsAlgebraic R h.root :=
  ⟨f, by simp [hf]⟩

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