lTensor_id_apply — Mathlib

English

Applying the right-tensor with the identity on the left yields the original tensor: (id_N).rTensor M x = x for x ∈ N ⊗ M.

Русский

Применение правого тензорирования к тождественному отображению даёт исходный тензор: (id_N).rTensor M x = x.

LaTeX

$$$(id_N).rTensor M (x) = x$$$

Lean4

theorem lTensor_id_apply (x : M ⊗[R] N) : (LinearMap.id : N →ₗ[R] N).lTensor M x = x := by
  rw [lTensor_id, id_coe, _root_.id]

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