L₂'_exact

Mathlib.Algebra.Homology.ShortComplex.SnakeLemma

URI: https://scilib.ai/kg/mathlib#CategoryTheory.ShortComplex.SnakeInput.L₂'_exact

← MathLib Explorer

English

The sequence L₂'.Exact holds, i.e., L0'' maps to L3'.

Русский

Последовательность L₂'.Exact верна; равнос— L0''→L3'.

LaTeX

$$$S.L₂'.Exact$$$

Lean4

/-- Exactness of `L₀.X₃ ⟶ L₃.X₁ ⟶ L₃.X₂`. -/
theorem L₂'_exact : S.L₂'.Exact := by
  rw [← exact_op_iff, exact_iff_of_iso S.L₂'OpIso]
  exact S.op.L₁'_exact

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

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

Разделы

MathLib Explorer
Graph RAG
Лаборатория
Блог
О проекте
Команда

Аффилиация

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