tensorProduct_apply'

Mathlib.LinearAlgebra.TensorProduct.Basis

URI: https://scilib.ai/kg/mathlib#Module.Basis.tensorProduct_apply'

English

For a base product, the basis element corresponding to i where i is a pair equals b i.1 ⊗ c i.2.

Русский

Для пары индексов i = (i1,i2) элемент базиса равен b_{i1} ⊗ c_{i2}.

LaTeX

$$$\tensorProduct b c (i) = b_{i.1} \otimes c_{i.2}$$$

Lean4

theorem tensorProduct_apply' (b : Basis ι S M) (c : Basis κ R N) (i : ι × κ) : tensorProduct b c i = b i.1 ⊗ₜ c i.2 :=
  by simp [tensorProduct]

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

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

Разделы

Аффилиация

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