Documentation

Mathlib.Algebra.Ring.NegOnePow

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.

source
def Int.negOnePow (n : ℤ) :
ℤˣ

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

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