PInfty_comp_QInfty

Mathlib.AlgebraicTopology.DoldKan.PInfty

URI: https://scilib.ai/kg/mathlib#AlgebraicTopology.DoldKan.PInfty_comp_QInfty

English

The global endomorphisms PInfty and QInfty annihilate each other: PInfty ∘ QInfty = 0.

Русский

Схождение PInfty и QInfty взаимно уничтожают друг друга: PInfty ∘ QInfty = 0.

LaTeX

$$$ PInfty \circ QInfty = 0 $$$

Lean4

@[reassoc (attr := simp)]
theorem PInfty_comp_QInfty : (PInfty : K[X] ⟶ _) ≫ QInfty = 0 :=
  by
  ext n
  apply PInfty_f_comp_QInfty_f

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

Научная платформа российской исследовательской школы.

Разделы

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru