English
For any x in L, the trace from L to the extension F equals the finiteness factor times the trace in the simple adjunction by x.
Русский
Для любого x в L след по построению над F равен размерности финитного расширения, умноженной на след в простой адильности по x.
LaTeX
$$$\\operatorname{trace}_{K,L}(x) = \\operatorname{finrank}_{K} K\\langle x\\rangle_L \\cdot \\operatorname{trace}_{K}( K\\langle x\\rangle , AdjoinSimple.gen\\,K\\,x)$$$
Lean4
theorem trace_eq_trace_adjoin [FiniteDimensional K L] (x : L) :
trace K L x = finrank K⟮x⟯ L • trace K K⟮x⟯ (AdjoinSimple.gen K x) :=
by
rw [← trace_trace (S := K⟮x⟯)]
conv in x => rw [← AdjoinSimple.algebraMap_gen K x]
rw [trace_algebraMap, LinearMap.map_smul_of_tower]
