instTensorSignsIntUp — Mathlib

English

A simplified expression of the permutation of signs in a tensor of two sign systems.

Русский

Упрощённое выражение перестановки знаков в тензоре двух систем знаков.

LaTeX

$$$\\varepsilon_2\\varepsilon_1 = -\\varepsilon_1\\varepsilon_2$ (symbolic relation under relations)$$

Lean4

instance : TensorSigns (ComplexShape.up ℤ)
    where
  ε' := MonoidHom.mk' Int.negOnePow Int.negOnePow_add
  rel_add p q r (hpq : p + 1 = q) := by dsimp; omega
  add_rel p q r (hpq : p + 1 = q) := by dsimp; omega
  ε'_succ := by
    rintro p _ rfl
    dsimp
    rw [Int.negOnePow_succ]

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