trace_tensorProduct' — Mathlib

English

A cyclic commutativity property: tr(g∘f) = tr(f∘g) for suitable endomorphisms f,g.

Русский

Циклическое свойство следа: tr(g∘f) = tr(f∘g) для подходящих концевых отображений.

LaTeX

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

Lean4

theorem trace_tensorProduct' (f : M →ₗ[R] M) (g : N →ₗ[R] N) : trace R (M ⊗ N) (map f g) = trace R M f * trace R N g :=
  by
  have h := LinearMap.ext_iff.1 (LinearMap.ext_iff.1 (trace_tensorProduct R M N) f) g
  simp only [compr₂_apply, mapBilinear_apply, compl₁₂_apply, lsmul_apply, Algebra.id.smul_eq_mul] at h
  exact h

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