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.

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
    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.coe_negOnePow (K : Type u_1) (n : ) [Field K] :
    n.negOnePow = (-1) ^ n