trace_transpose' — Mathlib

English

A variant of the tensor-product trace relation: tr_{M⊗N}(TensorProduct.map f g) = tr_M(f) · tr_N(g).

Русский

Вариант соотношения следа в тензорном произведении: tr_{M⊗N}(TensorProduct.map f g) = tr_M(f) · tr_N(g).

LaTeX

$$$ \operatorname{trace}_R (M \otimes N) ( \mathrm{TensorProduct.map} f g ) = \operatorname{trace}_R M f \cdot \operatorname{trace}_R N g. $$$

Lean4

@[simp]
theorem trace_transpose' (f : M →ₗ[R] M) : trace R _ (Module.Dual.transpose (R := R) f) = trace R M f := by
  rw [← comp_apply, trace_transpose]

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