toTensor_ι

Mathlib.LinearAlgebra.TensorAlgebra.Basic

URI: https://scilib.ai/kg/mathlib#FreeAlgebra.toTensor_ι

English

The image of FreeAlgebra.ι_R m under toTensor is exactly TensorAlgebra.ι_R m.

Русский

Образ FreeAlgebra.ι_R m под действием toTensor равен TensorAlgebra.ι_R m.

LaTeX

$$$\\text{toTensor}(\\mathrm{FreeAlgebra.ι}_R m) = \\mathrm{TensorAlgebra.ι}_R m$$$

Lean4

@[simp]
theorem toTensor_ι (m : M) : FreeAlgebra.toTensor (FreeAlgebra.ι R m) = TensorAlgebra.ι R m := by simp [toTensor]

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

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

Разделы

Аффилиация

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