σ — Mathlib · SciLib

English

The sign function σ is defined as the symmetry sign determined by the two ComplexShape components c1 and c2 relative to c12.

Русский

Знак σ определяется как знак симметрии, зависящий от компонент ComplexShape c1, c2 относительно c12.

LaTeX

$$$\\sigma(i_1,i_2) := TotalComplexShapeSymmetry.\\sigma\\, c_1\\, c_2\\, c_{12}\\; i_1\\; i_2.$$$

Lean4

/-- The signs involved in the symmetry isomorphism of the total complex. -/
abbrev σ (i₁ : I₁) (i₂ : I₂) : ℤˣ :=
  TotalComplexShapeSymmetry.σ c₁ c₂ c₁₂ i₁ i₂

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