Mathlib.Algebra.Ring.NegOnePow

Int.negOnePow definition

(n : ℤ) : ℤˣ

Full source

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

Integer power of $-1$ in the group of units

Informal description

The function maps an integer $ n $ to the $ n $-th power of $-1$ in the group of units of the integers, denoted as $(-1)^n \in \mathbb{Z}^\times$.

Int.negOnePow_def theorem

(n : ℤ) : n.negOnePow = (-1 : ℤˣ) ^ n

Full source

lemma negOnePow_def (n : ℤ) : n.negOnePow = (-1 : ℤℤˣ) ^ n := rfl

Definition of $\text{negOnePow}$ as $(-1)^n$ in the group of units

Informal description

For any integer $n$, the function $\text{negOnePow}(n)$ is equal to $(-1)^n$ in the group of units of the integers, i.e., $\text{negOnePow}(n) = (-1)^n$.

Int.negOnePow_add theorem

(n₁ n₂ : ℤ) : (n₁ + n₂).negOnePow = n₁.negOnePow * n₂.negOnePow

Full source

lemma negOnePow_add (n₁ n₂ : ℤ) :
    (n₁ + n₂).negOnePow =  n₁.negOnePow * n₂.negOnePow :=
  zpow_add _ _ _

Additive Property of Integer Powers of $-1$: $\text{negOnePow}(n_1 + n_2) = \text{negOnePow}(n_1) \cdot \text{negOnePow}(n_2)$

Informal description

For any integers $n_1$ and $n_2$, the function $\text{negOnePow}$ satisfies the additive property $\text{negOnePow}(n_1 + n_2) = \text{negOnePow}(n_1) \cdot \text{negOnePow}(n_2)$, where $\text{negOnePow}(n) = (-1)^n$ in the group of units of the integers.

Int.negOnePow_zero theorem

: negOnePow 0 = 1

Full source

@[simp]
lemma negOnePow_zero : negOnePow 0 = 1 := rfl

Zeroth Power of $-1$ in Integer Units Equals One

Informal description

The zeroth power of $-1$ in the group of units of the integers is equal to the multiplicative identity, i.e., $(-1)^0 = 1$.

Int.negOnePow_one theorem

: negOnePow 1 = -1

Full source

@[simp]
lemma negOnePow_one : negOnePow 1 = -1 := rfl

First Power of $-1$ in Units of Integers

Informal description

The first power of $-1$ in the group of units of the integers is $-1$, i.e., $(-1)^1 = -1$.

Int.negOnePow_succ theorem

(n : ℤ) : (n + 1).negOnePow = -n.negOnePow

Full source

lemma negOnePow_succ (n : ℤ) : (n + 1).negOnePow = - n.negOnePow := by
  rw [negOnePow_add, negOnePow_one, mul_neg, mul_one]

Recursive Formula for Integer Powers of $-1$: $(-1)^{n+1} = -(-1)^n$

Informal description

For any integer $n$, the $(n+1)$-th power of $-1$ in the group of units of the integers equals the negation of the $n$-th power, i.e., $(-1)^{n+1} = -(-1)^n$.

Int.negOnePow_even theorem

(n : ℤ) (hn : Even n) : n.negOnePow = 1

Full source

lemma negOnePow_even (n : ℤ) (hn : Even n) : n.negOnePow = 1 := by
  obtain ⟨k, rfl⟩ := hn
  rw [negOnePow_add, units_mul_self]

Even Powers of $-1$ Equal One: $(-1)^n = 1$ for Even $n$

Informal description

For any integer $n$ such that $n$ is even, the $n$-th power of $-1$ in the group of units of the integers equals $1$, i.e., $(-1)^n = 1$.

Int.negOnePow_two_mul theorem

(n : ℤ) : (2 * n).negOnePow = 1

Full source

@[simp]
lemma negOnePow_two_mul (n : ℤ) : (2 * n).negOnePow = 1 :=
  negOnePow_even _ ⟨n, two_mul n⟩

Even Integer Powers of $-1$: $(-1)^{2n} = 1$

Informal description

For any integer $n$, the $(2n)$-th power of $-1$ in the group of units of the integers equals $1$, i.e., $(-1)^{2n} = 1$.

Int.negOnePow_odd theorem

(n : ℤ) (hn : Odd n) : n.negOnePow = -1

Full source

lemma negOnePow_odd (n : ℤ) (hn : Odd n) : n.negOnePow = -1 := by
  obtain ⟨k, rfl⟩ := hn
  simp only [negOnePow_add, negOnePow_two_mul, negOnePow_one, mul_neg, mul_one]

Odd Powers of $-1$ Equal Negative One: $(-1)^n = -1$ for Odd $n$

Informal description

For any integer $n$ such that $n$ is odd, the $n$-th power of $-1$ in the group of units of the integers equals $-1$, i.e., $(-1)^n = -1$.

Int.negOnePow_two_mul_add_one theorem

(n : ℤ) : (2 * n + 1).negOnePow = -1

Full source

@[simp]
lemma negOnePow_two_mul_add_one (n : ℤ) : (2 * n + 1).negOnePow = -1 :=
  negOnePow_odd _ ⟨n, rfl⟩

Odd Integer Powers of $-1$: $(-1)^{2n+1} = -1$

Informal description

For any integer $n$, the $(2n + 1)$-th power of $-1$ in the group of units of the integers equals $-1$, i.e., $(-1)^{2n + 1} = -1$.

Int.negOnePow_eq_one_iff theorem

(n : ℤ) : n.negOnePow = 1 ↔ Even n

Full source

lemma negOnePow_eq_one_iff (n : ℤ) : n.negOnePow = 1 ↔ Even n := by
  constructor
  · intro h
    rw [← Int.not_odd_iff_even]
    intro h'
    simp only [negOnePow_odd _ h'] at h
    contradiction
  · exact negOnePow_even n

Characterization of Even Powers of $-1$: $(-1)^n = 1 \leftrightarrow \text{Even}(n)$

Informal description

For any integer $n$, the $n$-th power of $-1$ in the group of units of the integers equals $1$ if and only if $n$ is even, i.e., $(-1)^n = 1 \leftrightarrow \text{Even}(n)$.

Int.negOnePow_eq_neg_one_iff theorem

(n : ℤ) : n.negOnePow = -1 ↔ Odd n

Full source

lemma negOnePow_eq_neg_one_iff (n : ℤ) : n.negOnePow = -1 ↔ Odd n := by
  constructor
  · intro h
    rw [← Int.not_even_iff_odd]
    intro h'
    rw [negOnePow_even _ h'] at h
    contradiction
  · exact negOnePow_odd n

$(-1)^n = -1$ if and only if $n$ is odd

Informal description

For any integer $n$, the $n$-th power of $-1$ in the group of units of the integers equals $-1$ if and only if $n$ is odd, i.e., $(-1)^n = -1 \leftrightarrow n \text{ is odd}$.

Int.abs_negOnePow theorem

(n : ℤ) : |(n.negOnePow : ℤ)| = 1

Full source

@[simp]
theorem abs_negOnePow (n : ℤ) : |(n.negOnePow : ℤ)| = 1 := by
  rw [abs_eq_natAbs, Int.units_natAbs, Nat.cast_one]

Absolute Value of $(-1)^n$ is 1

Informal description

For any integer $n$, the absolute value of $(-1)^n$ (considered as an integer) equals 1, i.e., $|(-1)^n| = 1$.

Int.negOnePow_neg theorem

(n : ℤ) : (-n).negOnePow = n.negOnePow

Full source

@[simp]
lemma negOnePow_neg (n : ℤ) : (-n).negOnePow = n.negOnePow := by
  dsimp [negOnePow]
  simp only [zpow_neg, ← inv_zpow, inv_neg, inv_one]

$(-1)^{-n} = (-1)^n$ for integer $n$

Informal description

For any integer $n$, the $(-n)$-th power of $-1$ in the group of units of the integers equals the $n$-th power of $-1$, i.e., $(-1)^{-n} = (-1)^n$.

Int.negOnePow_abs theorem

(n : ℤ) : |n|.negOnePow = n.negOnePow

Full source

@[simp]
lemma negOnePow_abs (n : ℤ) : |n|.negOnePow = n.negOnePow := by
  obtain h|h := abs_choice n <;> simp only [h, negOnePow_neg]

Absolute Value Invariance of $(-1)^n$

Informal description

For any integer $n$, the power of $-1$ evaluated at the absolute value of $n$ equals the power of $-1$ evaluated at $n$, i.e., $(-1)^{|n|} = (-1)^n$.

Int.negOnePow_sub theorem

(n₁ n₂ : ℤ) : (n₁ - n₂).negOnePow = n₁.negOnePow * n₂.negOnePow

Full source

lemma negOnePow_sub (n₁ n₂ : ℤ) :
    (n₁ - n₂).negOnePow = n₁.negOnePow * n₂.negOnePow := by
  simp only [sub_eq_add_neg, negOnePow_add, negOnePow_neg]

Subtractive Property of Integer Powers of $-1$: $\text{negOnePow}(n_1 - n_2) = \text{negOnePow}(n_1) \cdot \text{negOnePow}(n_2)$

Informal description

For any integers $n_1$ and $n_2$, the function $\text{negOnePow}$ satisfies the property $\text{negOnePow}(n_1 - n_2) = \text{negOnePow}(n_1) \cdot \text{negOnePow}(n_2)$, where $\text{negOnePow}(n) = (-1)^n$ in the group of units of the integers.

Int.negOnePow_eq_iff theorem

(n₁ n₂ : ℤ) : n₁.negOnePow = n₂.negOnePow ↔ Even (n₁ - n₂)

Full source

lemma negOnePow_eq_iff (n₁ n₂ : ℤ) :
    n₁.negOnePow = n₂.negOnePow ↔ Even (n₁ - n₂) := by
  by_cases h₂ : Even n₂
  · rw [negOnePow_even _ h₂, Int.even_sub, negOnePow_eq_one_iff]
    tauto
  · rw [Int.not_even_iff_odd] at h₂
    rw [negOnePow_odd _ h₂, Int.even_sub, negOnePow_eq_neg_one_iff,
      ← Int.not_odd_iff_even, ← Int.not_odd_iff_even]
    tauto

Equality of Powers of $-1$: $(-1)^{n_1} = (-1)^{n_2} \leftrightarrow \text{Even}(n_1 - n_2)$

Informal description

For any integers $n_1$ and $n_2$, the equality $(-1)^{n_1} = (-1)^{n_2}$ holds in the group of units of the integers if and only if the difference $n_1 - n_2$ is even.

Int.negOnePow_mul_self theorem

(n : ℤ) : (n * n).negOnePow = n.negOnePow

Full source

@[simp]
lemma negOnePow_mul_self (n : ℤ) : (n * n).negOnePow = n.negOnePow := by
  simpa [mul_sub, negOnePow_eq_iff] using n.even_mul_pred_self

Power of $-1$ on squares: $(-1)^{n^2} = (-1)^n$

Informal description

For any integer $n$, the power of $-1$ in the group of units evaluated at $n \cdot n$ equals the power of $-1$ evaluated at $n$, i.e., $(-1)^{n \cdot n} = (-1)^n$.

Int.cast_negOnePow_natCast theorem

(R : Type*) [Ring R] (n : ℕ) : negOnePow n = (-1 : R) ^ n

Full source

lemma cast_negOnePow_natCast (R : Type*) [Ring R] (n : ℕ) : negOnePow n = (-1 : R) ^ n := by
  obtain ⟨k, rfl | rfl⟩ := Nat.even_or_odd' n <;> simp [pow_succ, pow_mul]

Natural Number Powers of $-1$ Preserved Under Ring Casting: $(-1)^n = (-1)^n$

Informal description

For any ring $R$ and any natural number $n$, the $n$-th power of $-1$ in the group of units of the integers, when cast to $R$, equals the $n$-th power of $-1$ in $R$, i.e., $(-1)^n = (-1)^n$ (where the left side is interpreted in $\mathbb{Z}^\times$ and the right side in $R$).

Int.coe_negOnePow_natCast theorem

(n : ℕ) : negOnePow n = (-1 : ℤ) ^ n

Full source

lemma coe_negOnePow_natCast (n : ℕ) : negOnePow n = (-1 : ℤ) ^ n := cast_negOnePow_natCast ..

Natural Number Powers of $-1$ in Units and Integers: $(-1)^n = (-1)^n$

Informal description

For any natural number $n$, the $n$-th power of $-1$ in the group of units of the integers equals the $n$-th power of $-1$ in the integers, i.e., $(-1)^n = (-1)^n$ (where the left side is interpreted in $\mathbb{Z}^\times$ and the right side in $\mathbb{Z}$).