hom_hom_associator — Mathlib

English

The isometry corresponding to the associator is equal to tensorAssoc: (α_ M N K).hom.toIsometry = (tensorAssoc _ _ _).toIsometry.

Русский

Изометрия ассоциатора равна изометрии тензорного сопряжения: (α_ M N K).hom.toIsometry = (tensorAssoc _ _ _).toIsometry.

LaTeX

$$$ (\alpha_ M N K).hom.toIsometry = (tensorAssoc _ _ _).toIsometry $$$

Lean4

theorem hom_hom_associator {M N K : QuadraticModuleCat.{u} R} :
    (α_ M N K).hom.toIsometry = (tensorAssoc _ _ _).toIsometry :=
  rfl

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