ε₂ — Mathlib

English

Similarly, the vertical differential of the total complex has a sign determined by ε2: I1 × I2 → ℤ×, assigning to each (i1, i2) a ±1 depending on the vertical component.

Русский

Аналогично, вертикальный дифференциал полной сложности имеет знак, заданный ε2: I1 × I2 → ℤ×, который сопоставляет каждому (i1, i2) знак ±1 в зависимости от вертикальной компоненты.

LaTeX

$$$\\varepsilon_2: I_1 \\times I_2 \\to \\mathbb{Z}^{\\times}$$$

Lean4

/-- The sign of the vertical differential in the total complex. -/
abbrev ε₂ (i : I₁ × I₂) : ℤˣ :=
  TotalComplexShape.ε₂ c₁ c₂ c₁₂ i

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