English
If x ∈ F is integral over R, then the trace from L to F of x is integral over R.
Русский
Если x ∈ F интегрирован над R, тогда след из L в F от x интегрирован над R.
LaTeX
$$$\\operatorname{IsIntegral}\\,R\\; (\\operatorname{trace}_{L,F}(x))$ whenever $x$ integral over R$$
Lean4
theorem isIntegral_trace [FiniteDimensional L F] {x : F} (hx : IsIntegral R x) : IsIntegral R (Algebra.trace L F x) :=
by
have hx' : IsIntegral L x := hx.tower_top
rw [← isIntegral_algebraMap_iff (algebraMap L (AlgebraicClosure F)).injective, trace_eq_sum_roots]
· refine (IsIntegral.multiset_sum ?_).nsmul _
intro y hy
rw [mem_roots_map (minpoly.ne_zero hx')] at hy
use minpoly R x, minpoly.monic hx
rw [← aeval_def] at hy ⊢
exact minpoly.aeval_of_isScalarTower R x y hy
· apply IsAlgClosed.splits_codomain
