assoc_toAlgEquiv — Mathlib

English

The associator as a bilinear equivalence matches the standard Algebra.TensorProduct.assoc when interpreted as an algebra-equivalence.

Русский

Ассоциатор как билигебра-эквивалентность совпадает со стандартной Algebra.TensorProduct.assoc как алгебра-эквивалентность.

LaTeX

$$$\text{assoc}_{R,S,A,C,D} : _ \equiv_[S] _ = \text{Algebra.TensorProduct.assoc} R S A C D$$$

Lean4

@[simp]
theorem assoc_toAlgEquiv :
    (Bialgebra.TensorProduct.assoc R S A C D : _ ≃ₐ[S] _) = Algebra.TensorProduct.assoc R S A C D :=
  rfl

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