assocRight — Mathlib

English

Right associator for HolorIndex: HolorIndex (ds₁ ++ ds₂ ++ ds₃) ≅ HolorIndex (ds₁ ++ (ds₂ ++ ds₃)).

Русский

Правая ассоциативность для HolorIndex: эквивалентности группировки индексов.

LaTeX

$$assocRight : HolorIndex (ds₁ ++ ds₂ ++ ds₃) → HolorIndex (ds₁ ++ (ds₂ ++ ds₃))$$

Lean4

/-- Right associator for `HolorIndex` -/
def assocRight : HolorIndex (ds₁ ++ ds₂ ++ ds₃) → HolorIndex (ds₁ ++ (ds₂ ++ ds₃)) :=
  cast (congr_arg HolorIndex (append_assoc ds₁ ds₂ ds₃))

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