English
Let F, E, K be fields with E and K integral over F and equipped with compatible algebra structures in a tower F ⊆ E ⊆ K. Then for every a ∈ E, the normalized trace from F to K applied to the image of a in K via E is equal to the normalized trace from F to E of a.
Русский
Пусть F, E, K — поля, у которых E и K являются целыми над F и задана совместимая структура алгебр в каскаде F ⊆ E ⊆ K. Тогда для каждого a ∈ E выполняется равенство: Tr_{F}^{K}(algebraMap_E^K(a)) = Tr_{F}^{E}(a).
LaTeX
$$$\\\\forall a \\\\in E:\\; \\,\\\\operatorname{normalizedTrace}_{F}^{K}(\\\\mathrm{algebraMap}_{E}^{K}(a)) \,=\, \\,\\\\operatorname{normalizedTrace}_{F}^{E}(a).$$
Lean4
@[simp]
theorem normalizedTrace_algebraMap_apply (a : E) : normalizedTrace F K (algebraMap E K a) = normalizedTrace F E a :=
normalizedTrace_map F K (IsScalarTower.toAlgHom F E K) a
