rTensor_id

Mathlib.LinearAlgebra.TensorProduct.Tower

URI: https://scilib.ai/kg/mathlib#TensorProduct.AlgebraTensorModule.rTensor_id

English

The RTensor construction sends the identity endomorphism to the identity endomorphism: rTensor R N (id : M →_A M) = id.

Русский

Конструкция RTensor отправляет единичное отображение в единичное отображение: rTensor R N (id : M →_A M) = id.

LaTeX

$$$rTensor\ R\ N\ (id : M \to_A M) = 1$$$

Lean4

@[simp]
theorem rTensor_id : rTensor R N (id : M →ₗ[A] M) = .id :=
  ext fun _ _ => rfl

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

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

Разделы

Аффилиация

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