rTensor_comp_map

Mathlib.LinearAlgebra.TensorProduct.Basic

URI: https://scilib.ai/kg/mathlib#LinearMap.rTensor_comp_map

← MathLib Explorer

English

—

Русский

—

LaTeX

$$$$ (f'\,\mathrm{rTensor}\,\_).\mathrm{comp}(\mathrm{map}\ f\ g) = \mathrm{map}(f'\circ f)\ g. $$$$

Lean4

@[simp]
theorem rTensor_comp_map (f' : P →ₗ[R] S) (f : M →ₗ[R] P) (g : N →ₗ[R] Q) :
    (f'.rTensor _).comp (map f g) = map (f'.comp f) g := by simp only [rTensor, ← map_comp, id_comp]

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

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

Разделы

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

Аффилиация

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