ε_down_ℕ

Mathlib.Algebra.Homology.ComplexShapeSigns

URI: https://scilib.ai/kg/mathlib#ComplexShape.ε_down_ℕ

English

The sign on ComplexShape.down ℕ at n equals (-1)^n.

Русский

Знак на ComplexShape.down ℕ в позиции n равен (-1)^n.

LaTeX

$$$(\\mathbb{C}\\text{ombined sign})$ at n equals $(-1)^n$$$

Lean4

@[simp]
theorem ε_down_ℕ (n : ℕ) : (ComplexShape.down ℕ).ε n = (-1 : ℤˣ) ^ n :=
  rfl

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

Научная платформа российской исследовательской школы.

Разделы

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru