w₀₂_τ₂

Mathlib.Algebra.Homology.ShortComplex.SnakeLemma

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

English

In a snake diagram, the composition along the second column satisfies w0τ2 = 0.

Русский

В змее композиция по второму столбцу равна нулю.

LaTeX

$$$S.v_{01}.\tau_2 \circ S.v_{12}.\tau_2 = 0$$$

Lean4

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

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

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

Разделы

Аффилиация

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