of_aeval_of_transcendental — Mathlib

English

If aeval r f is algebraic over R and f is transcendental over R, then r is algebraic over R.

Русский

Если aeval r f алгебраичен над R, а f трансцендентен над R, тогда r алгебраичен над R.

LaTeX

$$$ IsAlgebraic R (aeval r f) \to Transcendental R f \to IsAlgebraic R r $$$

Lean4

theorem of_aeval_of_transcendental {r : A} {f : R[X]} (H : IsAlgebraic R (aeval r f)) (hf : Transcendental R f) :
    IsAlgebraic R r := by
  contrapose H
  exact Transcendental.aeval_of_transcendental H hf

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