isAlgebraic_iff_not_injective — Mathlib

English

An element x is algebraic over R iff the evaluation map aeval x is not injective.

Русский

Элемент x алгебраичен над R тогда и только тогда, когда отображение aeval x не инъективно.

LaTeX

$$$ IsAlgebraic R x \leftrightarrow \neg Function.Injective (Polynomial.aeval x : R[X] \to_{R} A) $$$

Lean4

theorem isAlgebraic_iff_not_injective {x : A} :
    IsAlgebraic R x ↔ ¬Function.Injective (Polynomial.aeval x : R[X] →ₐ[R] A) := by
  simp only [IsAlgebraic, injective_iff_map_eq_zero, not_forall, and_comm, exists_prop]

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