English
Let R be a commutative ring and A an R-algebra. If for some positive integer n we have that r^n is algebraic over R, then r is algebraic over R.
Русский
Пусть R — коммутативное кольцо, A — R-алгебра. Если для некоторого положительного n элемент r^n алгебраичен над R, то и элемент r алгебраичен над R.
LaTeX
$$$\forall R\ A\ [\mathrm{CommRing}\ R] [\mathrm{Ring}\ A] [\mathrm{Algebra}\ R\ A]\n\forall r \in A, \forall n \in \mathbb{N}, 0 < n \Rightarrow (\mathrm{IsAlgebraic}\ R\ (r^n) \Rightarrow \mathrm{IsAlgebraic}\ R\ r)$$$
Lean4
theorem of_pow {r : A} {n : ℕ} (hn : 0 < n) (ht : IsAlgebraic R (r ^ n)) : IsAlgebraic R r :=
have ⟨p, p_nonzero, hp⟩ := ht
⟨_, by rwa [expand_ne_zero hn], by rwa [expand_aeval n p r]⟩
