QInfty_idem

Mathlib.AlgebraicTopology.DoldKan.PInfty

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

English

The endomorphism QInfty on K[X] is idempotent: QInfty ∘ QInfty = QInfty.

Русский

Идемпотент QInfty на K[X]: QInfty ∘ QInfty = QInfty.

LaTeX

$$$ QInfty \circ QInfty = QInfty $$$

Lean4

@[reassoc (attr := simp)]
theorem QInfty_idem : (QInfty : K[X] ⟶ _) ≫ QInfty = QInfty :=
  by
  ext n
  exact QInfty_f_idem n

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

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

Разделы

Аффилиация

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