trace_mul_cycle

Mathlib.LinearAlgebra.Trace

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

English

Trace of f g h equals trace of h f g, i.e., cyclic permutation preserves trace.

Русский

След от f g h равен следу h f g, т.е. циклическая перестановка сохраняет след.

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 [LinearMap.trace_mul_comm, ← mul_assoc]

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

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

Разделы

Аффилиация

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