trace_mul_comm — Mathlib

English

For endomorphisms f,g, the traces of fg and gf coincide: tr(fg) = tr(gf).

Русский

Следы произведений fg и gf совпадают: tr(fg) = tr(gf).

LaTeX

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

Lean4

theorem trace_mul_comm (f g : M →ₗ[R] M) : trace R M (f * g) = trace R M (g * f) := by
  classical
  by_cases H : ∃ s : Finset M, Nonempty (Basis s R M)
  · let ⟨s, ⟨b⟩⟩ := H
    simp_rw [trace_eq_matrix_trace R b, LinearMap.toMatrix_mul]
    apply Matrix.trace_mul_comm
  · rw [trace, dif_neg H, LinearMap.zero_apply, LinearMap.zero_apply]

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