English
Under suitable splitting, the trace equals the sum of all embeddings σ: L →ₐ[K] E applied to x.
Русский
При подходящем разложении след равен сумме значений всех вложений σ: L →ₐ[K] E применительно к x.
LaTeX
$$$\\operatorname{algebraMap}_{K,E}(\\operatorname{trace}_{K,L}(x)) = \\sum_{\\sigma : L \\to_{K} E} \\sigma(x)$$$
Lean4
theorem trace_eq_sum_roots [FiniteDimensional K L] {x : L} (hF : (minpoly K x).Splits (algebraMap K F)) :
algebraMap K F (Algebra.trace K L x) = finrank K⟮x⟯ L • ((minpoly K x).aroots F).sum := by
rw [trace_eq_trace_adjoin K x, Algebra.smul_def, RingHom.map_mul, ← Algebra.smul_def,
IntermediateField.AdjoinSimple.trace_gen_eq_sum_roots _ hF, IsScalarTower.algebraMap_smul]
