English
Let a ∈ K. If the minimal polynomial of a over E has all its coefficients in F (i.e., lies in the image of F under the embedding to E), then transporting the F-trace of a to E equals the E-trace of a from K to E.
Русский
Пусть a ∈ K. Если минимальный многочлен a над E имеет все коэффициенты в F (то есть лежит в образе F в E), тогда algebraMap_{F}^{E}(normalizedTrace_{F}^{K}(a)) = normalizedTrace_{E}^{K}(a).
LaTeX
$$$\\text{minpoly}_{E}(a) \\in \\text{Polynomial.lifts}(\\\\mathrm{algebraMap}_{F}^{E}) \\\\Rightarrow \\\\mathrm{algebraMap}_{F}^{E}(\\\\operatorname{normalizedTrace}_{F}^{K}(a)) = \\\\operatorname{normalizedTrace}_{E}^{K}(a) $$$
Lean4
@[simp]
theorem normalizedTrace_algebraMap : normalizedTrace F K ∘ₗ Algebra.linearMap E K = normalizedTrace F E :=
LinearMap.ext <| normalizedTrace_algebraMap_apply F E K
