baseChange_repr_tmul

Mathlib.LinearAlgebra.TensorProduct.Basis

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

← MathLib Explorer

English

The base-changed basis element at index i is 1 ⊗ b_i.

Русский

Элемент базиса после базового переноса по индексу i равен 1 ⊗ b_i.

LaTeX

$$$ (b.baseChange S) i = 1 \otimes b_i $$$

Lean4

@[simp]
theorem baseChange_repr_tmul (b : Basis ι R M) (x y i) : (b.baseChange S).repr (x ⊗ₜ y) i = b.repr y i • x := by
  simp [baseChange, tensorProduct]

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

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

Разделы

MathLib Explorer
Graph RAG
Лаборатория
Блог
О проекте
Команда

Аффилиация

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