associative_ε₁_eq_mul — Mathlib

English

The ε₁ signs satisfy a multiplicative associativity relation: ε₁ on the two-step concatenation equals the product of ε₁ on the inner step and ε₁ on the outer step.

Русский

Знаки ε₁ удовлетворяют ассоциативному соотношению умножения: знак на двойном шаге равен произведению знаков на внутреннем и внешнем шагах.

LaTeX

$$$\\varepsilon_1(c_1,c_2\\_23,c)(\\langle i_1, i_2+i_3\\rangle)=\\varepsilon_{12,3}(\\langle i_1,i_2\\rangle,i_3)\\cdot \\varepsilon_1(c_1,c_2,c_{12})(\\langle i_1,i_2\\rangle,i_3)$$$

Lean4

theorem associative_ε₁_eq_mul (i₁ : I₁) (i₂ : I₂) (i₃ : I₃) :
    ε₁ c₁ c₂₃ c (i₁, π c₂ c₃ c₂₃ (i₂, i₃)) = ε₁ c₁₂ c₃ c (π c₁ c₂ c₁₂ (i₁, i₂), i₃) * ε₁ c₁ c₂ c₁₂ (i₁, i₂) := by
  apply Associative.ε₁_eq_mul

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