lTensorBot_one_tmul

Mathlib.LinearAlgebra.TensorProduct.Subalgebra

URI: https://scilib.ai/kg/mathlib#Subalgebra.lTensorBot_one_tmul

English

The lTensorBot map sends 1 ⊗ a to a.

Русский

Отображение lTensorBot отправляет 1 ⊗ a в a.

LaTeX

$$$A.lTensorBot (1 \\otimes a) = a$$$

Lean4

@[simp]
theorem lTensorBot_one_tmul (a : A) : A.lTensorBot (1 ⊗ₜ[R] a) = a :=
  (toSubmodule A).lTensorOne_one_tmul a

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

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

Разделы

Аффилиация

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