trace_conj — Mathlib

English

Trace is invariant under conjugation by invertible endomorphisms: tr(f g f^{-1}) = tr(g).

Русский

След инвариантен относительно конъюгации инвертируемыми отображениями: tr(f g f^{-1}) = tr(g).

LaTeX

$$$\\operatorname{trace}_R M (f g f^{-1}) = \\operatorname{trace}_R M (g)$$$

Lean4

/-- The trace of an endomorphism is invariant under conjugation -/
@[simp]
theorem trace_conj (g : M →ₗ[R] M) (f : (M →ₗ[R] M)ˣ) : trace R M (↑f * g * ↑f⁻¹) = trace R M g :=
  by
  rw [trace_mul_comm]
  simp

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