trace_self

Mathlib.RingTheory.Trace.Defs

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

← MathLib Explorer

English

The trace map from R to R is the identity map.

Русский

Следовая карта от R к самому R есть тождественное отображение.

LaTeX

$$$\\operatorname{trace}(R,R) = \\mathrm{id}$$$

Lean4

/-- The trace map from `R` to itself is the identity map. -/
@[simp]
theorem trace_self : trace R R = LinearMap.id := by ext; simpa using trace_algebraMap_of_basis (.singleton (Fin 1) R) 1

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

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

Разделы

MathLib Explorer
Graph RAG
Лаборатория
Блог
О проекте
Команда

Аффилиация

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