lTensor_map

Mathlib.LinearAlgebra.TensorProduct.Basic

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

← MathLib Explorer

English

—

Русский

—

LaTeX

$$$$ (f.rTensor N)^n = (f^n).rTensor N. $$$$

Lean4

@[simp]
theorem lTensor_map (g' : Q →ₗ[R] S) (f : M →ₗ[R] P) (g : N →ₗ[R] Q) (x : M ⊗[R] N) :
    g'.lTensor P (map f g x) = map f (g' ∘ₗ g) x :=
  LinearMap.congr_fun (lTensor_comp_map _ _ f g) x

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

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

Разделы

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

Аффилиация

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