negOnePow

Mathlib.Algebra.Ring.NegOnePow

URI: https://scilib.ai/kg/mathlib#Int.negOnePow

English

There is a canonical map negOnePow: ℤ → ℤˣ sending n to (-1)ⁿ.

Русский

Существуют каноническое отображение negOnePow: ℤ → ℤˣ, отправляющее n в (-1)ⁿ.

LaTeX

$$$\mathrm{negOnePow}: \mathbb{Z} \to \mathbb{Z}^{\times},\ n \mapsto (-1)^{n}$$$

Lean4

/-- The map `ℤ → ℤˣ` which sends `n` to `(-1 : ℤˣ) ^ n`. -/
def negOnePow (n : ℤ) : ℤˣ :=
  (-1 : ℤˣ) ^ n

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

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

Разделы

Аффилиация

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