assoc_eq

Mathlib.LinearAlgebra.TensorProduct.Tower

URI: https://scilib.ai/kg/mathlib#TensorProduct.AlgebraTensorModule.assoc_eq

← MathLib Explorer

English

The heterobasic associator coincides with the standard TensorProduct.assoc.

Русский

Гетеробазовый ассоциатор совпадает с обычной ассоциацией TensorProduct.

LaTeX

$$$\text{assoc}_{R,A,B} = \text{TensorProduct.assoc}$$$

Lean4

/-- The heterobasic version of `assoc` coincides with the regular version. -/
theorem assoc_eq : assoc R R R M P Q = TensorProduct.assoc R M P Q :=
  rfl

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

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

Разделы

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

Аффилиация

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