tensorLId_apply

Mathlib.LinearAlgebra.QuadraticForm.TensorProduct.Isometries

URI: https://scilib.ai/kg/mathlib#QuadraticForm.tensorLId_apply

English

The same associativity map equality holds pointwise: (tensorAssoc Q1 Q2 Q3) x = TensorProduct.assoc x.

Русский

То же самое в точечном виде: (tensorAssoc Q1 Q2 Q3) x = TensorProduct.assoc x.

LaTeX

$$$(tensorAssoc\, Q_1\, Q_2\, Q_3)\, x = (TensorProduct.assoc\, R\, M_1\, M_2\, M_3)\, x$$$

Lean4

@[simp]
theorem tensorLId_apply (Q₂ : QuadraticForm R M₂) (x : R ⊗[R] M₂) : tensorLId Q₂ x = TensorProduct.lid R M₂ x :=
  rfl

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

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

Разделы

Аффилиация

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