English
If r ∈ A and f ∈ R[X] satisfy the hypotheses, and aeval r f is algebraic over R, then r is algebraic over R.
Русский
Если r ∈ A и f ∈ R[X] удовлетворяют условиям, и aeval r f алгебраичен над R, то r алгебраичен над R.
LaTeX
$$$ \forall r : A,\ f : R[X],\ f.natDegree \neq 0 \to f.leadingCoeff \in R^0 \to IsAlgebraic R (aeval r f) \to IsAlgebraic R r $$$
Lean4
theorem of_aeval {r : A} (f : R[X]) (hf : f.natDegree ≠ 0) (hf' : f.leadingCoeff ∈ R⁰) (H : IsAlgebraic R (aeval r f)) :
IsAlgebraic R r := by
obtain ⟨p, h1, h2⟩ := H
have : (p.comp f).coeff (p.natDegree * f.natDegree) ≠ 0 := fun h ↦
h1 <| by
rwa [coeff_comp_degree_mul_degree hf, mul_right_mem_nonZeroDivisors_eq_zero_iff (pow_mem hf' _),
leadingCoeff_eq_zero] at h
exact ⟨p.comp f, fun h ↦ this (by simp [h]), by rwa [aeval_comp]⟩
