assoc — Mathlib

English

For a ∈ A, b ∈ C, c ∈ D, the associator satisfies: assoc((a ⊗ b) ⊗ c) = a ⊗ (b ⊗ c).

Русский

Для a ∈ A, b ∈ C, c ∈ D ассоциатор даёт: assoc((a ⊗ b) ⊗ c) = a ⊗ (b ⊗ c).

LaTeX

$$$ \\operatorname{assoc}_{R,S,A,C,D}( (a \\otimes b) \\otimes c ) = a \\otimes (b \\otimes c) $$$

Lean4

/-- The associator for tensor product of R-algebras, as an algebra isomorphism. -/
protected def assoc : A ⊗[S] C ⊗[R] D ≃ₐ[S] A ⊗[S] (C ⊗[R] D) :=
  AlgEquiv.ofLinearEquiv (AlgebraTensorModule.assoc R S S A C D) (by simp [Algebra.TensorProduct.one_def])
    ((LinearMap.map_mul_iff _).mpr <| by ext; simp)

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