mkHom_f_0

Mathlib.Algebra.Homology.HomologicalComplex

URI: https://scilib.ai/kg/mathlib#CochainComplex.mkHom_f_0

English

The degree-0 component of mkHom is zero-morphism on P.X0 → Q.X0.

Русский

Компонента mkHom в нулевой степени является нулевым морфизмом.

LaTeX

$$$\\mathrm{mkHom}.f_0 = \\mathrm{zero}$$$

Lean4

@[simp]
theorem mkHom_f_0 : (mkHom P Q zero one one_zero_comm succ).f 0 = zero :=
  rfl

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

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

Разделы

Аффилиация

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