rTensor_add

Mathlib.LinearAlgebra.TensorProduct.Basic

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

English

Right-tensoring is linear in the map argument: (f+g).rTensor M = f.rTensor M + g.rTensor M for f,g: N →ₗ[R] P.

Русский

Правотензорирование линейно по отображению: (f+g).rTensor M = f.rTensor M + g.rTensor M.

LaTeX

$$$(f+g).rTensor M = f.rTensor M + g.rTensor M$$$

Lean4

@[simp]
theorem rTensor_add (f g : N →ₗ[R] P) : (f + g).rTensor M = f.rTensor M + g.rTensor M :=
  (rTensorHom M).map_add f g

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

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

Разделы

Аффилиация

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