normalizedTrace_algebraMap_apply_eq_self

Mathlib.FieldTheory.NormalizedTrace

URI: https://scilib.ai/kg/mathlib#Algebra.normalizedTrace_algebraMap_apply_eq_self

English

For a ∈ F, the normalized trace from F to K of its image in K equals a itself.

Русский

Пусть a ∈ F. Тогда нормализованный след от образа a в K равен самому a.

LaTeX

$$$\\operatorname{normalizedTrace}_{F}^{K}(\\\\mathrm{algebraMap}_{F}^{K}(a)) = a \\\\text{ for all } a \\in F$$$

Lean4

theorem normalizedTrace_algebraMap_apply_eq_self (a : F) : normalizedTrace F K (algebraMap F K a) = a := by simp

Похожие утверждения

Научная платформа российской исследовательской школы.

Разделы

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru