D₁_D₂ — Mathlib

English

The cross terms D1 and D2 anticommute: D1 ∘ D2 = - D2 ∘ D1.

Русский

Кросс-термы D1 и D2 антикоммутируют: D1 ∘ D2 = - D2 ∘ D1.

LaTeX

$$$K.D_1 c_{12} i_{12} i_{12}' \\;\\circ\\; K.D_2 c_{12} i_{12}' i_{12}'' = -\\; K.D_2 c_{12} i_{12} i_{12}' \\;\\circ\\; K.D_1 c_{12} i_{12}' i_{12}''$$$

Lean4

@[reassoc]
theorem D₁_D₂ (i₁₂ i₁₂' i₁₂'' : I₁₂) :
    K.D₁ c₁₂ i₁₂ i₁₂' ≫ K.D₂ c₁₂ i₁₂' i₁₂'' = -K.D₂ c₁₂ i₁₂ i₁₂' ≫ K.D₁ c₁₂ i₁₂' i₁₂'' := by simp

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