map_one

Mathlib.LinearAlgebra.PiTensorProduct

URI: https://scilib.ai/kg/mathlib#PiTensorProduct.map_one

English

The map of the constant endomorphism 1 is the identity endomorphism on the tensor product.

Русский

Отображение от единичного тензорного отображения даёт единичное отображение на тензорном произведении.

LaTeX

$$$\mathrm{map}\, (\lambda i, 1_{s_i}) = 1$$$

Lean4

@[simp]
protected theorem map_one : map (fun (i : ι) ↦ (1 : s i →ₗ[R] s i)) = 1 :=
  map_id

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

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

Разделы

Аффилиация

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