w₁₃_τ₃

Mathlib.Algebra.Homology.ShortComplex.SnakeLemma

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

English

The composition S.v12.τ1 with S.v23.τ1 is zero in the snake input.

Русский

Композиция S.v12.τ1 с S.v23.τ1 равна нулю в входе змейки.

LaTeX

$$$S.v_{12}.\tau_1 \circ S.v_{23}.\tau_1 = 0$$$

Lean4

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

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

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

Разделы

Аффилиация

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