d₁_eq_zero' — Mathlib

English

If the π-entry does not match the target, D1 is zero by totalAux reasoning.

Русский

Если запись π не совпадает с целевым индексом, D1 равно нулю по рассуждению totalAux.

LaTeX

$$$\\text{(h' : ComplexShape.π c_{1} c_{2} c_{1 2} \\langle i_1', i_2 \\rangle \\neq i_{12})} \\Rightarrow K.D_{1} c_{12} i_{1} i_{2} i_{12} = 0$$$

Lean4

theorem d₁_eq_zero' {i₁ i₁' : I₁} (h : c₁.Rel i₁ i₁') (i₂ : I₂) (i₁₂ : I₁₂)
    (h' : ComplexShape.π c₁ c₂ c₁₂ ⟨i₁', i₂⟩ ≠ i₁₂) : K.d₁ c₁₂ i₁ i₂ i₁₂ = 0 :=
  by
  rw [totalAux.d₁_eq' K c₁₂ h i₂ i₁₂, K.toGradedObject.ιMapObjOrZero_eq_zero, comp_zero, smul_zero]
  exact h'

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