trace_self_apply

Mathlib.RingTheory.Trace.Defs

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

English

For any a ∈ R, trace_R_R(a) = a.

Русский

Для любого a ∈ R след R,R(a) = a.

LaTeX

$$$\\operatorname{trace}(R,R)(a) = a$$$

Lean4

theorem trace_self_apply (a) : trace R R a = a := by simp

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

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

Разделы

Аффилиация

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