# Integer powers of (-1) #

This file defines the map negOnePow : ℤ → ℤˣ which sends n to (-1 : ℤˣ) ^ n.

The definition of negOnePow and some lemmas first appeared in contributions by Johan Commelin to the Liquid Tensor Experiment.

def Int.negOnePow (n : ) :

The map ℤ → ℤˣ which sends n to (-1 : ℤˣ) ^ n.

Equations
• n.negOnePow = (-1) ^ n
Instances For
theorem Int.negOnePow_def (n : ) :
n.negOnePow = (-1) ^ n
theorem Int.negOnePow_add (n₁ : ) (n₂ : ) :
(n₁ + n₂).negOnePow = n₁.negOnePow * n₂.negOnePow
@[simp]
theorem Int.negOnePow_zero :
0.negOnePow = 1
@[simp]
theorem Int.negOnePow_one :
1.negOnePow = -1
theorem Int.negOnePow_succ (n : ) :
(n + 1).negOnePow = -n.negOnePow
theorem Int.negOnePow_even (n : ) (hn : Even n) :
n.negOnePow = 1
@[simp]
theorem Int.negOnePow_two_mul (n : ) :
(2 * n).negOnePow = 1
theorem Int.negOnePow_odd (n : ) (hn : Odd n) :
n.negOnePow = -1
@[simp]
theorem Int.negOnePow_two_mul_add_one (n : ) :
(2 * n + 1).negOnePow = -1
theorem Int.negOnePow_eq_one_iff (n : ) :
n.negOnePow = 1 Even n
theorem Int.negOnePow_eq_neg_one_iff (n : ) :
n.negOnePow = -1 Odd n
@[simp]
theorem Int.negOnePow_neg (n : ) :
(-n).negOnePow = n.negOnePow
theorem Int.negOnePow_sub (n₁ : ) (n₂ : ) :
(n₁ - n₂).negOnePow = n₁.negOnePow * n₂.negOnePow
theorem Int.negOnePow_eq_iff (n₁ : ) (n₂ : ) :
n₁.negOnePow = n₂.negOnePow Even (n₁ - n₂)
@[simp]
theorem Int.negOnePow_mul_self (n : ) :
(n * n).negOnePow = n.negOnePow
theorem Int.coe_negOnePow (K : Type u_1) (n : ) [] :
n.negOnePow = (-1) ^ n