assoc_tmul

Mathlib.RingTheory.TensorProduct.Basic

URI: https://scilib.ai/kg/mathlib#Algebra.TensorProduct.assoc_tmul

English

The associator is an algebra isomorphism A ⊗_S C ⊗_R D ≃_S A ⊗_S (C ⊗_R D).

Русский

Ассоциатор является изоморфизмом алгебр: A ⊗_S C ⊗_R D ≃_S A ⊗_S (C ⊗_R D).

LaTeX

$$$ A \\otimes_S C \\otimes_R D \\cong_S A \\otimes_S (C \\otimes_R D) $$$

Lean4

@[simp]
theorem assoc_tmul (a : A) (b : C) (c : D) : TensorProduct.assoc R S A C D ((a ⊗ₜ b) ⊗ₜ c) = a ⊗ₜ (b ⊗ₜ c) :=
  rfl

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

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

Разделы

Аффилиация

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