trace_eq_contract_apply — Mathlib

English

For x in M^* ⊗_R M, the trace applied to the image of x under the dual-tensor–to–linear map equals the contraction of x with x itself.

Русский

Для x ∈ M^* ⊗_R M выполнено tr((dualTensorHom) x) = contractLeft x.

LaTeX

$$$ \operatorname{trace}_R(M) \bigl( (\mathrm{dualTensorHom}_R(M,M))x \bigr) = \mathrm{contractLeft}_R(M)\,x. $$$

Lean4

@[simp]
theorem trace_eq_contract_apply (x : Module.Dual R M ⊗[R] M) :
    (LinearMap.trace R M) ((dualTensorHom R M M) x) = contractLeft R M x := by rw [← comp_apply, trace_eq_contract]

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