lTensor_id

Mathlib.LinearAlgebra.TensorProduct.Basic

URI: https://scilib.ai/kg/mathlib#LinearMap.lTensor_id

English

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

Русский

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

LaTeX

$$$(lTensor M\, id_N)(x) = x$$$

Lean4

@[simp]
theorem lTensor_id : (id : N →ₗ[R] N).lTensor M = id :=
  map_id

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

Научная платформа российской исследовательской школы.

Разделы

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru