w₀₂_τ₃

Mathlib.Algebra.Homology.ShortComplex.SnakeLemma

URI: https://scilib.ai/kg/mathlib#CategoryTheory.ShortComplex.SnakeInput.w₀₂_τ₃

English

The upper part of the first column in the snake diagram is exact.

Русский

Верхняя часть первой колонки в змее диаграммы точна.

LaTeX

$$$(\text{Upper first column}) \text{ is exact}$$$

Lean4

@[reassoc (attr := simp)]
theorem w₀₂_τ₃ : S.v₀₁.τ₃ ≫ S.v₁₂.τ₃ = 0 := by rw [← comp_τ₃, S.w₀₂, zero_τ₃]

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

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

Разделы

Аффилиация

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