QInfty_f_comp_PInfty_f — Mathlib

English

For each degree n, the composition QInfty.f n with PInfty.f n is zero.

Русский

Для каждого n композиция QInfty.f n с PInfty.f n равна нулю.

LaTeX

$$$ (QInfty.f n) \circ (PInfty.f n) = 0 $$$

Lean4

@[reassoc (attr := simp)]
theorem QInfty_f_comp_PInfty_f (n : ℕ) : (QInfty.f n : X _⦋n⦌ ⟶ _) ≫ PInfty.f n = 0 :=
  by
  dsimp only [QInfty]
  simp only [HomologicalComplex.sub_f_apply, HomologicalComplex.id_f, sub_comp, id_comp, PInfty_f_idem, sub_self]

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