ιTotalOrZero_eq — Mathlib

English

If the π-index does not match the target index, the inclusion ιTotal vanishes.

Русский

Если индекс π не совпадает с целевым индексом, включение ιTotal нулевое.

LaTeX

$$$\\text{If } c_1 c_2 c_{12} (i_1,i_2) \\neq i_{12}, \\; ιTotal c_{12} i_1 i_2 i_{12} = 0$$$

Lean4

theorem ιTotalOrZero_eq (i₁ : I₁) (i₂ : I₂) (i₁₂ : I₁₂) (h : ComplexShape.π c₁ c₂ c₁₂ (i₁, i₂) = i₁₂) :
    K.ιTotalOrZero c₁₂ i₁ i₂ i₁₂ = K.ιTotal c₁₂ i₁ i₂ i₁₂ h :=
  dif_pos h

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