add

Mathlib.LinearAlgebra.TensorProduct.Basic

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

English

Addition on the tensor product is induced by bilinearity: (m1 + m2) ⊗ n = m1 ⊗ n + m2 ⊗ n for all m1, m2 ∈ M and n ∈ N.

Русский

Сложение в тензорном произведении задаётся билинейностью: (m1 + m2) ⊗ n = m1 ⊗ n + m2 ⊗ n.

LaTeX

$$$ (m_1 + m_2) \\otimes_R n = m_1 \\otimes_R n + m_2 \\otimes_R n. $$$

Lean4

protected instance add : Add (M ⊗[R] N) :=
  (addConGen (TensorProduct.Eqv R M N)).hasAdd

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

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

Разделы

Аффилиация

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