Q_zero

Mathlib.AlgebraicTopology.DoldKan.Projections

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

English

The degree-wise component applicative rule for natTransPInfty_f ensures compatibility with evaluation maps.

Русский

Правило применения компонент natTransPInfty_f в степени (2) обеспечивает совместимость с отображениями оценки.

LaTeX

$$$ (natTransPInfty_f)_n = PInfty.f n$$$

Lean4

@[simp]
theorem Q_zero : (Q 0 : K[X] ⟶ _) = 0 :=
  sub_self _

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

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

Разделы

Аффилиация

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