piScalarRightHom_tmul

Mathlib.LinearAlgebra.TensorProduct.Pi

URI: https://scilib.ai/kg/mathlib#TensorProduct.piScalarRightHom_tmul

← MathLib Explorer

English

The action on tmul is given by mapping to a function sending i ↦ x ⊗ f(i).

Русский

Действие на tmul задаётся отображением i ↦ x ⊗ f(i).

LaTeX

$$$piRightHom_R S N M (x \otimes f) = (i \mapsto x \otimes f(i)).$$$

Lean4

@[simp]
theorem piScalarRightHom_tmul (x : N) (f : ι → R) : piScalarRightHom R S N ι (x ⊗ₜ f) = (fun j ↦ f j • x) :=
  by
  ext j
  simp [piScalarRightHom, piScalarRightHomBil]

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

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

Разделы

MathLib Explorer
Graph RAG
Лаборатория
Блог
О проекте
Команда

Аффилиация

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