coe_lTensor

Mathlib.LinearAlgebra.TensorProduct.Tower

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

English

Restricting scalars commutes with lTensor; the restricted map equals the lTensor map of f.

Русский

Ограничение скаляров коммутирует с lTensor; ограниченное отображение равно lTensor отображению f.

LaTeX

$$$ (lTensor\; A\; M\; f).restrictScalars R = f.lTensor M$$$

Lean4

@[simp]
theorem coe_lTensor (f : N →ₗ[R] Q) : (lTensor A M f : M ⊗[R] N → M ⊗[R] Q) = f.lTensor M :=
  rfl

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

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

Разделы

Аффилиация

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