homTensorHomMap_apply

Mathlib.LinearAlgebra.TensorProduct.Basic

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

English

Tensor product mapping is compatible with smul on maps: map (r • f) g = r • map f g.

Русский

Совместимо с умножением на скаляр: map (r • f) g = r • map f g.

LaTeX

$$$\\operatorname{map}(r \\cdot f) g = r \\cdot \\operatorname{map} f g$$$

Lean4

@[simp]
theorem homTensorHomMap_apply (f : M →ₗ[R] P) (g : N →ₗ[R] Q) : homTensorHomMap R M N P Q (f ⊗ₜ g) = map f g :=
  rfl

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

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

Разделы

Аффилиация

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