associative_ε₂_ε₁ — Mathlib

English

The combination of ε₂ and ε₁ satisfies an associativity identity in the total complex, aligning with how horizontal and vertical signs interact when grouping three factors.

Русский

Сочетание ε₂ и ε₁ удовлетворяет тождеству ассоциативности в полном комплексе, согласуясь с тем, как горизонтальные и вертикальные знаки взаимодействуют при группировке трёх факторов.

LaTeX

$$$\\text{associative\_ε₂\_ε₁}(i_1,i_2,i_3)=\\text{ε₂ε₁ in total}(i_1,i_2,i_3)$$$

Lean4

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

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