normalizedTrace_self

Mathlib.FieldTheory.NormalizedTrace

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

English

The normalized trace on the base field is the identity map.

Русский

Нормализованный след на базовом поле является тождественным отображением.

LaTeX

$$$\text{normalizedTrace } F F = \mathrm{Id}$$$

Lean4

@[simp]
theorem normalizedTrace_self : normalizedTrace F F = LinearMap.id :=
  LinearMap.ext normalizedTrace_self_apply

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

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

Разделы

Аффилиация

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