baseChange_apply

Mathlib.LinearAlgebra.TensorProduct.Basis

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

English

For i in ι and j in κ, (tensorProduct b c) (i,j) equals b_i ⊗ c_j.

Русский

Для i ∈ ι и j ∈ κ, (tensorProduct b c)(i,j) = b_i ⊗ c_j.

LaTeX

$$$ (tensorProduct b c) (i,j) = b_i \otimes c_j $$$

Lean4

@[simp]
theorem baseChange_apply (b : Basis ι R M) (i) : b.baseChange S i = 1 ⊗ₜ b i := by simp [baseChange, tensorProduct]

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

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

Разделы

Аффилиация

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