L₃_exact

Mathlib.Algebra.Homology.ShortComplex.SnakeLemma

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

English

In a SnakeInput diagram within an abelian category, the third level L₃ is exact.

Русский

В диаграмме SnakeInput в абелевой категории третий уровень L₃ является точной.

LaTeX

$$$$ S.L_3.Exact $$$$

Lean4

theorem L₃_exact : S.L₃.Exact :=
  S.op.L₀_exact.unop

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

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

Разделы

Аффилиация

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