English
If y is not nilpotent and y z is integral over R, then z is algebraic over R.
Русский
Если y не нильпотентно и y z интегрально над R, то z алгебраическая над R.
LaTeX
$$$\neg IsNilpotent(y) \land IsIntegral R (y \cdot z) \Rightarrow Algebra.IsAlgebraic R z$$$
Lean4
theorem of_smul_isIntegral {y : R} (hy : ¬IsNilpotent y) (h : IsIntegral R (y • z)) : IsAlgebraic R z :=
by
have ⟨p, monic, eval0⟩ := h
refine ⟨p.comp (C y * X), fun h ↦ ?_, by simpa [aeval_comp, Algebra.smul_def] using eval0⟩
apply_fun (coeff · p.natDegree) at h
have hy0 : y ≠ 0 := by rintro rfl; exact hy .zero
rw [coeff_zero, ← mul_one p.natDegree, ← natDegree_C_mul_X y hy0, coeff_comp_degree_mul_degree, monic, one_mul,
leadingCoeff_C_mul_X] at h
· exact hy ⟨_, h⟩
· rw [natDegree_C_mul_X _ hy0]; rintro ⟨⟩
