PInfty_f_0

Mathlib.AlgebraicTopology.DoldKan.PInfty

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

English

QInfty is the limit-defining endomorphism on K[X] given by QInfty = Id − PInfty.

Русский

QInfty — пределостной энтоморфизм на K[X], задающийся как QInfty = Id − PInfty.

LaTeX

$$$QInfty = \mathrm{Id} - PInfty$$$

Lean4

@[simp]
theorem PInfty_f_0 : (PInfty.f 0 : X _⦋0⦌ ⟶ X _⦋0⦌) = 𝟙 _ :=
  rfl

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

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

Разделы

Аффилиация

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