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.

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 : negOnePow 0 = 1

@[simp]

theorem Int.negOnePow_one : negOnePow 1 = -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.abs_negOnePow (n : ℤ) : |↑n.negOnePow| = 1

@[simp]

theorem Int.negOnePow_neg (n : ℤ) : (-n).negOnePow = n.negOnePow

@[simp]

theorem Int.negOnePow_abs (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.cast_negOnePow_natCast (R : Type u_1) [Ring R] (n : ℕ) : ↑↑(↑n).negOnePow = (-1) ^ n

theorem Int.coe_negOnePow_natCast (n : ℕ) : ↑(↑n).negOnePow = (-1) ^ n