δ_L₃_f

Mathlib.Algebra.Homology.ShortComplex.SnakeLemma

URI: https://scilib.ai/kg/mathlib#CategoryTheory.ShortComplex.SnakeInput.δ_L₃_f

English

The composition δ with L₃.f is zero.

Русский

Сочетание δ с L₃.f равно нулю.

LaTeX

$$$S.\\delta \\circ S.L_3.f = 0$$$

Lean4

theorem δ_L₃_f : S.δ ≫ S.L₃.f = 0 := by
  rw [← cancel_epi S.L₀'.g]
  erw [S.L₀'_exact.g_desc_assoc]
  simp [S.v₂₃.comm₁₂, φ₂]

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

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

Разделы

Аффилиация

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