transcendental_iff_injective — Mathlib

English

An element x is transcendental over R exactly when the map aeval x is injective.

Русский

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

LaTeX

$$$ Transcendental R x \iff Function.Injective (Polynomial.aeval x : R[X] \to_{R} A) $$$

Lean4

/-- An element `x` is transcendental over `R` if and only if the map `Polynomial.aeval x`
is injective. This is similar to `algebraicIndependent_iff_injective_aeval`. -/
theorem transcendental_iff_injective {x : A} :
    Transcendental R x ↔ Function.Injective (Polynomial.aeval x : R[X] →ₐ[R] A) :=
  isAlgebraic_iff_not_injective.not_left

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