mk₀_zero

Mathlib.CategoryTheory.Shift.ShiftedHom

URI: https://scilib.ai/kg/mathlib#CategoryTheory.ShiftedHom.mk₀_zero

English

mk₀ with m₀ and hm₀ = 0 yields a canonical zero ShiftedHom morphism.

Русский

mk₀ с m₀ и hm₀ = 0 даёт канонический нулевой ShiftedHom морфизм.

LaTeX

$$theorem mk₀_zero (X : C) (Y : C) (m₀ : M) (hm₀ : m₀ = 0) : mk₀ m₀ hm₀ (0 : X ⟶ Y) = 0$$

Lean4

@[simp]
theorem mk₀_zero (m₀ : M) (hm₀ : m₀ = 0) : mk₀ m₀ hm₀ (0 : X ⟶ Y) = 0 := by simp [mk₀]

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

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

Разделы

Аффилиация

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