instTensorSignsNatDown — Mathlib

English

The sign system on ComplexShape.down for ℕ is defined by ε' mapping n to (-1)^n with the usual properties of a TensorSigns instance.

Русский

Система знаков на ComplexShape.down для ℕ задана отображением ε'(n) = (-1)^n и обладает свойствами TensorSigns.

LaTeX

$$$\\text{signs}_{\\downarrow\\,\\mathbb{N}} : (\\mathbb{N},+) \\to \\mathbb{Z}^{\\times}$ with ε' (n)=(-1)^n$$

Lean4

instance : TensorSigns (ComplexShape.down ℕ)
    where
  ε' := MonoidHom.mk' (fun (i : ℕ) => (-1 : ℤˣ) ^ i) (pow_add (-1 : ℤˣ))
  rel_add p q r (hpq : q + 1 = p) := by dsimp; omega
  add_rel p q r (hpq : q + 1 = p) := by dsimp; omega
  ε'_succ := by
    rintro _ q rfl
    dsimp
    rw [pow_add, pow_one, mul_neg, mul_one, neg_neg]

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