trace_comp_cycle' — Mathlib

English

A variant of the cyclic trace identity, derived from trace_comp_comm' and associativity.

Русский

Вариант циклического трафа, полученный из trace_comp_comm' и ассоциативности.

LaTeX

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

Lean4

theorem trace_comp_cycle' (f : M →ₗ[R] N) (g : N →ₗ[R] P) (h : P →ₗ[R] M) :
    trace R P ((g ∘ₗ f) ∘ₗ h) = trace R M ((h ∘ₗ g) ∘ₗ f) := by rw [trace_comp_comm', ← comp_assoc]

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