trace_mul_cycle'

Mathlib.LinearAlgebra.Trace

URI: https://scilib.ai/kg/mathlib#LinearMap.trace_mul_cycle'

English

For endomorphisms f,g,h, the trace is invariant under cycling: tr(fgh) = tr(hfg).

Русский

След циклически инвариантен: tr(fgh) = tr(hfg).

LaTeX

$$$\\operatorname{trace}_R M (f g h) = \\operatorname{trace}_R M (h f g)$$$

Lean4

theorem trace_mul_cycle' (f g h : M →ₗ[R] M) : trace R M (f * (g * h)) = trace R M (h * (f * g)) := by
  rw [← mul_assoc, LinearMap.trace_mul_comm]

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

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

Разделы

Аффилиация

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