instTotalComplexShapeSymmetryIntUp

English

The sign function is symmetric in its arguments: σ c2 c1 c12 i2 i1 = σ c1 c2 c12 i1 i2.

Русский

Знак σ симметричен по аргументам: σ(c2,c1,c12)(i2,i1) = σ(c1,c2,c12)(i1,i2).

LaTeX

$$$\\sigma c_2 c_1 c_{12} i_2 i_1 = \\sigma c_1 c_2 c_{12} i_1 i_2.$$$

Lean4

@[simps]
instance : TotalComplexShapeSymmetry (up ℤ) (up ℤ) (up ℤ)
    where
  symm p q := add_comm q p
  σ p q := (p * q).negOnePow
  σ_ε₁ := by
    rintro p _ rfl q
    dsimp
    rw [mul_one, ← Int.negOnePow_add, add_comm q, add_mul, one_mul, Int.negOnePow_add, Int.negOnePow_add, mul_assoc,
      Int.units_mul_self, mul_one]
  σ_ε₂ := by
    rintro p q _ rfl
    dsimp
    rw [one_mul, ← Int.negOnePow_add, mul_add, mul_one]

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