pow — Mathlib

English

If S is integral over R and a is algebraic over S, then a is algebraic over R.

Русский

Если S интегрально над R и a алгебраический над S, то a алгебраический над R.

LaTeX

$$[int : Algebra.IsIntegral R S] {a : A} (h : IsAlgebraic S a) : IsAlgebraic R a$$

Lean4

protected theorem pow (n : ℕ) : IsAlgebraic R (a ^ n) :=
  have := ha.nontrivial
  n.rec (pow_zero a ▸ isAlgebraic_one) fun _ h ↦ pow_succ a _ ▸ h.mul ha

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