assoc_toLinearEquiv — Mathlib

English

There is an algebra isomorphism A ⊗_S (C ⊗_R D) ≅_S A ⊗_S (C ⊗_R D) given by the associator, i.e., (A ⊗_S C) ⊗_R D ≅ 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_toLinearEquiv : (TensorProduct.assoc R S A C D).toLinearEquiv = AlgebraTensorModule.assoc R S S A C D :=
  rfl

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