doc-next-gen

Mathlib.Algebra.Ring.Parity

Module docstring

{"# Even and odd elements in rings

This file defines odd elements and proves some general facts about even and odd elements of rings.

As opposed to Even, Odd does not have a multiplicative counterpart.

TODO

Try to generalize Even lemmas further. For example, there are still a few lemmas whose Semiring assumptions I (DT) am not convinced are necessary. If that turns out to be true, they could be moved to Mathlib.Algebra.Group.Even.

See also

Mathlib.Algebra.Group.Even for the definition of even elements. "}

Even.neg_pow theorem
: Even n → ∀ a : α, (-a) ^ n = a ^ n
Full source 
@[simp] lemma Even.neg_pow : Even n → ∀ a : α, (-a) ^ n = a ^ n := by
  rintro ⟨c, rfl⟩ a
  simp_rw [← two_mul, pow_mul, neg_sq]
Even Power of Negative Element: $(-a)^n = a^n$ for even $n$
Informal description
For any even natural number $n$ and any element $a$ in a ring $\alpha$, the $n$-th power of $-a$ equals the $n$-th power of $a$, i.e., $(-a)^n = a^n$.
Even.neg_one_pow theorem
(h : Even n) : (-1 : α) ^ n = 1
Full source 
lemma Even.neg_one_pow (h : Even n) : (-1 : α) ^ n = 1 := by rw [h.neg_pow, one_pow]
Even Power of Negative One: $(-1)^n = 1$ for even $n$
Informal description
For any even natural number $n$ and in any ring $\alpha$, the $n$-th power of $-1$ equals $1$, i.e., $(-1)^n = 1$.
Even.neg_zpow theorem
: Even n → ∀ a : α, (-a) ^ n = a ^ n
Full source 
lemma Even.neg_zpow : Even n → ∀ a : α, (-a) ^ n = a ^ n := by
  rintro ⟨c, rfl⟩ a; simp_rw [← Int.two_mul, zpow_mul, zpow_two, neg_mul_neg]
Even Power of Negative Element Equals Power of Element: $(-a)^n = a^n$ for even $n$
Informal description
For any even integer $n$ and any element $a$ in a division monoid $\alpha$, the $n$-th power of $-a$ equals the $n$-th power of $a$, i.e., $(-a)^n = a^n$.
Even.neg_one_zpow theorem
(h : Even n) : (-1 : α) ^ n = 1
Full source 
lemma Even.neg_one_zpow (h : Even n) : (-1 : α) ^ n = 1 := by rw [h.neg_zpow, one_zpow]
Even Power of Negative One Equals One: $(-1)^n = 1$ for even $n$
Informal description
For any even integer $n$ and in any division monoid $\alpha$, the $n$-th power of $-1$ equals $1$, i.e., $(-1)^n = 1$.
IsSquare.zero theorem
[MulZeroClass α] : IsSquare (0 : α)
Full source 
@[simp] lemma IsSquare.zero [MulZeroClass α] : IsSquare (0 : α) := ⟨0, (mul_zero _).symm⟩
Zero is a square in any multiplicative monoid with zero
Informal description
In any multiplicative monoid with zero $\alpha$ (i.e., satisfying $0 \cdot a = 0$ and $a \cdot 0 = 0$ for all $a \in \alpha$), the zero element is a square. That is, there exists an element $r \in \alpha$ such that $0 = r \cdot r$.
even_iff_two_dvd theorem
: Even a ↔ 2 ∣ a
Full source 
lemma even_iff_two_dvd : EvenEven a ↔ 2 ∣ a := by simp [Even, Dvd.dvd, two_mul]
Characterization of Even Elements via Divisibility by 2
Informal description
An element $a$ in a semiring is even if and only if $2$ divides $a$.
Even.trans_dvd theorem
(ha : Even a) (hab : a ∣ b) : Even b
Full source 
lemma Even.trans_dvd (ha : Even a) (hab : a ∣ b) : Even b :=
  even_iff_two_dvd.2 <| ha.two_dvd.trans hab
Evenness is Transitive under Divisibility
Informal description
If an element $a$ in a semiring is even and $a$ divides $b$, then $b$ is also even.
Dvd.dvd.even theorem
(hab : a ∣ b) (ha : Even a) : Even b
Full source 
lemma Dvd.dvd.even (hab : a ∣ b) (ha : Even a) : Even b := ha.trans_dvd hab
Divisibility Preserves Evenness
Informal description
For any elements $a$ and $b$ in a semiring, if $a$ divides $b$ and $a$ is even, then $b$ is also even.
range_two_mul theorem
(α) [NonAssocSemiring α] : Set.range (fun x : α ↦ 2 * x) = {a | Even a}
Full source 
@[simp] lemma range_two_mul (α) [NonAssocSemiring α] :
    Set.range (fun x : α ↦ 2 * x) = {a | Even a} := by
  ext x
  simp [eq_comm, two_mul, Even]
Range of Doubling Function Equals Set of Even Elements in a Semiring
Informal description
Let $\alpha$ be a non-associative semiring. The range of the function $x \mapsto 2x$ is equal to the set of even elements in $\alpha$, i.e., \[ \text{range}(\lambda x, 2x) = \{a \in \alpha \mid \text{Even } a\}. \]
even_two theorem
: Even (2 : α)
Full source 
@[simp] lemma even_two : Even (2 : α) := ⟨1, by rw [one_add_one_eq_two]⟩
Evenness of Two in a Semiring
Informal description
For any semiring $\alpha$, the element $2$ is even, i.e., $2$ can be written as $2 = 2 \cdot k$ for some $k \in \alpha$.
Even.mul_left theorem
(ha : Even a) (b) : Even (b * a)
Full source 
@[simp] lemma Even.mul_left (ha : Even a) (b) : Even (b * a) := ha.map (AddMonoidHom.mulLeft _)
Left Multiplication Preserves Evenness
Informal description
For any elements $a$ and $b$ in a semiring $\alpha$, if $a$ is even, then the product $b \cdot a$ is also even.
Even.mul_right theorem
(ha : Even a) (b) : Even (a * b)
Full source 
@[simp] lemma Even.mul_right (ha : Even a) (b) : Even (a * b) := ha.map (AddMonoidHom.mulRight _)
Evenness is preserved under right multiplication
Informal description
For any elements $a$ and $b$ in a semiring $\alpha$, if $a$ is even, then the product $a \cdot b$ is also even.
even_two_mul theorem
(a : α) : Even (2 * a)
Full source 
lemma even_two_mul (a : α) : Even (2 * a) := ⟨a, two_mul _⟩
Double of any element is even
Informal description
For any element $a$ in a semiring $\alpha$, the element $2a$ is even.
Even.pow_of_ne_zero theorem
(ha : Even a) : ∀ {n : ℕ}, n ≠ 0 → Even (a ^ n)
Full source 
lemma Even.pow_of_ne_zero (ha : Even a) : ∀ {n : ℕ}, n ≠ 0 → Even (a ^ n)
  | n + 1, _ => by rw [pow_succ]; exact ha.mul_left _
Even Powers of Even Elements are Even
Informal description
For any element $a$ in a semiring $\alpha$, if $a$ is even, then for any nonzero natural number $n$, the power $a^n$ is also even.
Odd definition
(a : α) : Prop
Full source 
/-- An element `a` of a semiring is odd if there exists `k` such `a = 2*k + 1`. -/
def Odd (a : α) : Prop := ∃ k, a = 2 * k + 1
Odd element in a semiring
Informal description
An element $a$ of a semiring $\alpha$ is called *odd* if there exists an element $k \in \alpha$ such that $a = 2k + 1$.
odd_iff_exists_bit1 theorem
: Odd a ↔ ∃ b, a = 2 * b + 1
Full source 
lemma odd_iff_exists_bit1 : OddOdd a ↔ ∃ b, a = 2 * b + 1 := exists_congr fun b ↦ by rw [two_mul]
Characterization of Odd Elements: $a$ is odd iff $a = 2b + 1$ for some $b$
Informal description
An element $a$ in a semiring $\alpha$ is odd if and only if there exists an element $b \in \alpha$ such that $a = 2b + 1$.
range_two_mul_add_one theorem
(α : Type*) [Semiring α] : Set.range (fun x : α ↦ 2 * x + 1) = {a | Odd a}
Full source 
@[simp] lemma range_two_mul_add_one (α : Type*) [Semiring α] :
    Set.range (fun x : α ↦ 2 * x + 1) = {a | Odd a} := by ext x; simp [Odd, eq_comm]
Characterization of Odd Elements as Range of $2x + 1$ in a Semiring
Informal description
Let $\alpha$ be a semiring. The range of the function $x \mapsto 2x + 1$ is equal to the set of all odd elements of $\alpha$, i.e., \[ \{2x + 1 \mid x \in \alpha\} = \{a \in \alpha \mid \text{$a$ is odd}\}. \]
Even.add_odd theorem
: Even a → Odd b → Odd (a + b)
Full source 
lemma Even.add_odd : Even a → Odd b → Odd (a + b) := by
  rintro ⟨a, rfl⟩ ⟨b, rfl⟩; exact ⟨a + b, by rw [mul_add, ← two_mul, add_assoc]⟩
Sum of Even and Odd Elements is Odd
Informal description
For any elements $a$ and $b$ in a semiring $\alpha$, if $a$ is even and $b$ is odd, then their sum $a + b$ is odd.
Even.odd_add theorem
(ha : Even a) (hb : Odd b) : Odd (b + a)
Full source 
lemma Even.odd_add (ha : Even a) (hb : Odd b) : Odd (b + a) := add_comm a b ▸ ha.add_odd hb
Sum of Odd and Even Elements is Odd
Informal description
For any elements $a$ and $b$ in a semiring $\alpha$, if $a$ is even and $b$ is odd, then their sum $b + a$ is odd.
Odd.add_even theorem
(ha : Odd a) (hb : Even b) : Odd (a + b)
Full source 
lemma Odd.add_even (ha : Odd a) (hb : Even b) : Odd (a + b) := add_comm a b ▸ hb.add_odd ha
Sum of Odd and Even Elements is Odd
Informal description
For any elements $a$ and $b$ in a semiring $\alpha$, if $a$ is odd and $b$ is even, then their sum $a + b$ is odd.
Odd.add_odd theorem
: Odd a → Odd b → Even (a + b)
Full source 
lemma Odd.add_odd : Odd a → Odd b → Even (a + b) := by
  rintro ⟨a, rfl⟩ ⟨b, rfl⟩
  refine ⟨a + b + 1, ?_⟩
  rw [two_mul, two_mul]
  ac_rfl
Sum of Two Odd Elements is Even
Informal description
For any elements $a$ and $b$ in a semiring $\alpha$, if both $a$ and $b$ are odd, then their sum $a + b$ is even.
Even.add_one theorem
(h : Even a) : Odd (a + 1)
Full source 
@[simp] lemma Even.add_one (h : Even a) : Odd (a + 1) := h.add_odd odd_one
Even Element Plus One is Odd
Informal description
For any element $a$ in a semiring $\alpha$, if $a$ is even, then $a + 1$ is odd.
Even.one_add theorem
(h : Even a) : Odd (1 + a)
Full source 
@[simp] lemma Even.one_add (h : Even a) : Odd (1 + a) := h.odd_add odd_one
Sum of One and Even Element is Odd
Informal description
For any element $a$ in a semiring $\alpha$, if $a$ is even, then $1 + a$ is odd.
Odd.add_one theorem
(h : Odd a) : Even (a + 1)
Full source 
@[simp] lemma Odd.add_one (h : Odd a) : Even (a + 1) := h.add_odd odd_one
Odd element plus one is even
Informal description
For any element $a$ in a semiring $\alpha$, if $a$ is odd, then $a + 1$ is even.
Odd.one_add theorem
(h : Odd a) : Even (1 + a)
Full source 
@[simp] lemma Odd.one_add (h : Odd a) : Even (1 + a) := odd_one.add_odd h
Sum of One and Odd Element is Even
Informal description
For any odd element $a$ in a semiring $\alpha$, the element $1 + a$ is even.
odd_two_mul_add_one theorem
(a : α) : Odd (2 * a + 1)
Full source 
lemma odd_two_mul_add_one (a : α) : Odd (2 * a + 1) := ⟨_, rfl⟩
Odd Elements of the Form $2a + 1$ in a Semiring
Informal description
For any element $a$ in a semiring $\alpha$, the element $2a + 1$ is odd.
odd_add_self_one' theorem
: Odd (a + (a + 1))
Full source 
@[simp] lemma odd_add_self_one' : Odd (a + (a + 1)) := by simp [← add_assoc]
Oddity of $a + (a + 1)$ in a semiring
Informal description
For any element $a$ in a semiring $\alpha$, the element $a + (a + 1)$ is odd.
odd_add_one_self theorem
: Odd (a + 1 + a)
Full source 
@[simp] lemma odd_add_one_self : Odd (a + 1 + a) := by simp [add_comm _ a]
Oddness of $a + 1 + a$ in a semiring
Informal description
For any element $a$ in a semiring $\alpha$, the element $a + 1 + a$ is odd.
odd_add_one_self' theorem
: Odd (a + (1 + a))
Full source 
@[simp] lemma odd_add_one_self' : Odd (a + (1 + a)) := by simp [add_comm 1 a]
Sum of an element with its successor is odd
Informal description
For any element $a$ in a semiring $\alpha$, the element $a + (1 + a)$ is odd.
Odd.map theorem
[FunLike F α β] [RingHomClass F α β] (f : F) : Odd a → Odd (f a)
Full source 
lemma Odd.map [FunLike F α β] [RingHomClass F α β] (f : F) : Odd a → Odd (f a) := by
  rintro ⟨a, rfl⟩; exact ⟨f a, by simp [two_mul]⟩
Ring Homomorphism Preserves Odd Elements
Informal description
Let $\alpha$ and $\beta$ be semirings, and let $F$ be a type of functions from $\alpha$ to $\beta$ that preserves the ring structure (i.e., $F$ is a `RingHomClass`). For any function $f \in F$ and any odd element $a \in \alpha$, the image $f(a) \in \beta$ is also odd.
Odd.natCast theorem
{R : Type*} [Semiring R] {n : ℕ} (hn : Odd n) : Odd (n : R)
Full source 
lemma Odd.natCast {R : Type*} [Semiring R] {n : ℕ} (hn : Odd n) : Odd (n : R) :=
  hn.map <| Nat.castRingHom R
Canonical homomorphism preserves oddness of natural numbers
Informal description
Let $R$ be a semiring and $n$ be a natural number. If $n$ is odd (i.e., there exists a natural number $k$ such that $n = 2k + 1$), then the image of $n$ under the canonical ring homomorphism from $\mathbb{N}$ to $R$ is also odd in $R$.
Odd.mul theorem
: Odd a → Odd b → Odd (a * b)
Full source 
@[simp] lemma Odd.mul : Odd a → Odd b → Odd (a * b) := by
  rintro ⟨a, rfl⟩ ⟨b, rfl⟩
  refine ⟨2 * a * b + b + a, ?_⟩
  rw [mul_add, add_mul, mul_one, ← add_assoc, one_mul, mul_assoc, ← mul_add, ← mul_add, ← mul_assoc,
    ← Nat.cast_two, ← Nat.cast_comm]
Product of Odd Elements is Odd
Informal description
For any elements $a$ and $b$ in a semiring $\alpha$, if both $a$ and $b$ are odd (i.e., there exist $k_1, k_2 \in \alpha$ such that $a = 2k_1 + 1$ and $b = 2k_2 + 1$), then their product $a \cdot b$ is also odd.
Odd.pow theorem
(ha : Odd a) : ∀ {n : ℕ}, Odd (a ^ n)
Full source 
lemma Odd.pow (ha : Odd a) : ∀ {n : ℕ}, Odd (a ^ n)
  | 0 => by
    rw [pow_zero]
    exact odd_one
  | n + 1 => by rw [pow_succ]; exact ha.pow.mul ha
Odd Powers of Odd Elements Remain Odd
Informal description
Let $\alpha$ be a semiring and let $a \in \alpha$ be an odd element (i.e., there exists $k \in \alpha$ such that $a = 2k + 1$). Then for any natural number $n$, the power $a^n$ is also odd.
Odd.pow_add_pow_eq_zero theorem
[IsCancelAdd α] (hn : Odd n) (hab : a + b = 0) : a ^ n + b ^ n = 0
Full source 
lemma Odd.pow_add_pow_eq_zero [IsCancelAdd α] (hn : Odd n) (hab : a + b = 0) :
    a ^ n + b ^ n = 0 := by
  obtain ⟨k, rfl⟩ := hn
  induction k with | zero => simpa | succ k ih => ?_
  have : a ^ 2 = b ^ 2 := add_right_cancel <|
    calc
      a ^ 2 + a * b = 0 := by rw [sq, ← mul_add, hab, mul_zero]
      _ = b ^ 2 + a * b := by rw [sq, ← add_mul, add_comm, hab, zero_mul]
  refine add_right_cancel (b := b ^ (2 * k + 1) * a ^ 2) ?_
  calc
    _ = (a ^ (2 * k + 1) + b ^ (2 * k + 1)) * a ^ 2 + b ^ (2 * k + 3) := by
      rw [add_mul, ← pow_add, add_right_comm]; rfl
    _ = _ := by rw [ih, zero_mul, zero_add, zero_add, this, ← pow_add]
Odd Power Sum Vanishing for Additive Inverses: $a + b = 0 \Rightarrow a^n + b^n = 0$ for odd $n$
Informal description
Let $\alpha$ be a semiring with cancellative addition. For any odd natural number $n$ and any elements $a, b \in \alpha$ such that $a + b = 0$, we have $a^n + b^n = 0$.
Odd.neg_pow theorem
: Odd n → ∀ a : α, (-a) ^ n = -a ^ n
Full source 
lemma Odd.neg_pow : Odd n → ∀ a : α, (-a) ^ n = -a ^ n := by
  rintro ⟨c, rfl⟩ a; simp_rw [pow_add, pow_mul, neg_sq, pow_one, mul_neg]
Odd Power of Negative Element: $(-a)^n = -a^n$ for odd $n$
Informal description
Let $\alpha$ be a ring and let $n$ be an odd natural number. Then for any element $a \in \alpha$, the $n$-th power of $-a$ equals the negation of the $n$-th power of $a$, i.e., $(-a)^n = -a^n$.
Odd.neg_one_pow theorem
(h : Odd n) : (-1 : α) ^ n = -1
Full source 
@[simp] lemma Odd.neg_one_pow (h : Odd n) : (-1 : α) ^ n = -1 := by rw [h.neg_pow, one_pow]
Odd Power of Negative One: $(-1)^n = -1$ for odd $n$
Informal description
For any odd natural number $n$ and in any ring $\alpha$, the $n$-th power of $-1$ equals $-1$, i.e., $(-1)^n = -1$.
even_neg_two theorem
: Even (-2 : α)
Full source 
lemma even_neg_two : Even (-2 : α) := by simp only [even_neg, even_two]
Negation of Two is Even in Any Ring
Informal description
For any ring $\alpha$, the element $-2$ is even.
odd_neg_one theorem
: Odd (-1 : α)
Full source 
lemma odd_neg_one : Odd (-1 : α) := by simp
Negation of One is Odd in a Ring
Informal description
In any ring $\alpha$, the element $-1$ is odd, i.e., there exists an element $k \in \alpha$ such that $-1 = 2k + 1$.
Odd.sub_even theorem
(ha : Odd a) (hb : Even b) : Odd (a - b)
Full source 
lemma Odd.sub_even (ha : Odd a) (hb : Even b) : Odd (a - b) := by
  rw [sub_eq_add_neg]; exact ha.add_even hb.neg
Difference of Odd and Even Elements is Odd
Informal description
For any elements $a$ and $b$ in a ring $\alpha$, if $a$ is odd and $b$ is even, then their difference $a - b$ is odd.
Even.sub_odd theorem
(ha : Even a) (hb : Odd b) : Odd (a - b)
Full source 
lemma Even.sub_odd (ha : Even a) (hb : Odd b) : Odd (a - b) := by
  rw [sub_eq_add_neg]; exact ha.add_odd hb.neg
Difference of Even and Odd Elements is Odd
Informal description
For any elements $a$ and $b$ in a ring $\alpha$, if $a$ is even and $b$ is odd, then their difference $a - b$ is odd.
Odd.sub_odd theorem
(ha : Odd a) (hb : Odd b) : Even (a - b)
Full source 
lemma Odd.sub_odd (ha : Odd a) (hb : Odd b) : Even (a - b) := by
  rw [sub_eq_add_neg]; exact ha.add_odd hb.neg
Difference of Two Odd Elements is Even
Informal description
For any elements $a$ and $b$ in a ring $\alpha$, if both $a$ and $b$ are odd, then their difference $a - b$ is even.
Nat.instDecidablePredOdd instance
: DecidablePred (Odd : ℕ → Prop)
Full source 
instance : DecidablePred (Odd : ℕ → Prop) := fun _ ↦ decidable_of_iff _ odd_iff.symm
Decidability of Oddness for Natural Numbers
Informal description
For any natural number $n$, the property of being odd is decidable. That is, there exists an algorithm that can determine whether $n$ is odd or not.
Nat.not_odd_zero theorem
: ¬Odd 0
Full source 
@[simp] lemma not_odd_zero : ¬Odd 0 := not_odd_iff.mpr rfl
Zero is Not Odd
Informal description
The natural number $0$ is not odd, i.e., $\neg \text{Odd}(0)$.
Nat.even_xor_odd theorem
(n : ℕ) : Xor' (Even n) (Odd n)
Full source 
lemma even_xor_odd (n : ℕ) : Xor' (Even n) (Odd n) := by
  simp [Xor', ← not_even_iff_odd, Decidable.em (Even n)]
Exclusive Disjunction of Even and Odd for Natural Numbers
Informal description
For any natural number $n$, exactly one of the following holds: either $n$ is even or $n$ is odd, but not both.
Nat.even_or_odd theorem
(n : ℕ) : Even n ∨ Odd n
Full source 
lemma even_or_odd (n : ℕ) : EvenEven n ∨ Odd n := (even_xor_odd n).or
Every Natural Number is Even or Odd
Informal description
For any natural number $n$, either $n$ is even or $n$ is odd.
Nat.even_xor_odd' theorem
(n : ℕ) : ∃ k, Xor' (n = 2 * k) (n = 2 * k + 1)
Full source 
lemma even_xor_odd' (n : ℕ) : ∃ k, Xor' (n = 2 * k) (n = 2 * k + 1) := by
  obtain ⟨k, rfl⟩ | ⟨k, rfl⟩ := even_or_odd n <;> use k
  · simpa only [← two_mul, eq_self_iff_true, xor_true] using (succ_ne_self (2 * k)).symm
  · simpa only [xor_true, xor_comm] using (succ_ne_self _)
Exclusive-or Decomposition of Natural Numbers into Even or Odd
Informal description
For every natural number $n$, there exists a natural number $k$ such that exactly one of the following holds: either $n = 2k$ or $n = 2k + 1$.
Nat.mod_two_add_add_odd_mod_two theorem
(m : ℕ) {n : ℕ} (hn : Odd n) : m % 2 + (m + n) % 2 = 1
Full source 
lemma mod_two_add_add_odd_mod_two (m : ℕ) {n : ℕ} (hn : Odd n) : m % 2 + (m + n) % 2 = 1 :=
  ((even_or_odd m).elim fun hm ↦ by rw [even_iff.1 hm, odd_iff.1 (hm.add_odd hn)]) fun hm ↦ by
    rw [odd_iff.1 hm, even_iff.1 (hm.add_odd hn)]
Sum of Remainders Modulo 2 for $m$ and $m + n$ When $n$ is Odd
Informal description
For any natural numbers $m$ and $n$, if $n$ is odd, then the sum of the remainders when $m$ and $m + n$ are divided by 2 equals 1, i.e., $m \bmod 2 + (m + n) \bmod 2 = 1$.
Nat.mod_two_add_succ_mod_two theorem
(m : ℕ) : m % 2 + (m + 1) % 2 = 1
Full source 
@[simp] lemma mod_two_add_succ_mod_two (m : ℕ) : m % 2 + (m + 1) % 2 = 1 :=
  mod_two_add_add_odd_mod_two m odd_one
Sum of Remainders Modulo 2 for Successive Natural Numbers
Informal description
For any natural number $m$, the sum of the remainders when $m$ and $m + 1$ are divided by 2 equals 1, i.e., $m \bmod 2 + (m + 1) \bmod 2 = 1$.
Nat.succ_mod_two_add_mod_two theorem
(m : ℕ) : (m + 1) % 2 + m % 2 = 1
Full source 
@[simp] lemma succ_mod_two_add_mod_two (m : ℕ) : (m + 1) % 2 + m % 2 = 1 := by
  rw [add_comm, mod_two_add_succ_mod_two]
Sum of Remainders Modulo 2 for Successive Natural Numbers is One
Informal description
For any natural number $m$, the sum of the remainders when $m + 1$ and $m$ are divided by 2 equals 1, i.e., $(m + 1) \bmod 2 + m \bmod 2 = 1$.
Nat.even_add' theorem
: Even (m + n) ↔ (Odd m ↔ Odd n)
Full source 
lemma even_add' : EvenEven (m + n) ↔ (Odd m ↔ Odd n) := by
  rw [even_add, ← not_odd_iff_even, ← not_odd_iff_even, not_iff_not]
Parity of Sum via Oddness: $\text{Even}(m + n) \leftrightarrow (\text{Odd}(m) \leftrightarrow \text{Odd}(n))$
Informal description
For any natural numbers $m$ and $n$, the sum $m + n$ is even if and only if $m$ is odd exactly when $n$ is odd. In other words, $\text{Even}(m + n) \leftrightarrow (\text{Odd}(m) \leftrightarrow \text{Odd}(n))$.
Nat.not_even_bit1 theorem
(n : ℕ) : ¬Even (2 * n + 1)
Full source 
@[simp] lemma not_even_bit1 (n : ℕ) : ¬Even (2 * n + 1) := by simp [parity_simps]
Odd natural numbers are not even
Informal description
For any natural number $n$, the number $2n + 1$ is not even.
Nat.even_sub' theorem
(h : n ≤ m) : Even (m - n) ↔ (Odd m ↔ Odd n)
Full source 
lemma even_sub' (h : n ≤ m) : EvenEven (m - n) ↔ (Odd m ↔ Odd n) := by
  rw [even_sub h, ← not_odd_iff_even, ← not_odd_iff_even, not_iff_not]
Parity of Difference under Oddness: $\text{Even}(m - n) \leftrightarrow (\text{Odd}(m) \leftrightarrow \text{Odd}(n))$ for $n \leq m$
Informal description
For any natural numbers $n$ and $m$ with $n \leq m$, the difference $m - n$ is even if and only if $m$ is odd exactly when $n$ is odd, i.e., $\text{Even}(m - n) \leftrightarrow (\text{Odd}(m) \leftrightarrow \text{Odd}(n))$.
Nat.Odd.sub_odd theorem
(hm : Odd m) (hn : Odd n) : Even (m - n)
Full source 
lemma Odd.sub_odd (hm : Odd m) (hn : Odd n) : Even (m - n) :=
  (le_total n m).elim (fun h ↦ by simp only [even_sub' h, *]) fun h ↦ by
    simp only [Nat.sub_eq_zero_iff_le.2 h, Even.zero]
Difference of Odd Natural Numbers is Even
Informal description
For any natural numbers $m$ and $n$, if both $m$ and $n$ are odd, then their difference $m - n$ is even.
Nat.odd_mul theorem
: Odd (m * n) ↔ Odd m ∧ Odd n
Full source 
lemma odd_mul : OddOdd (m * n) ↔ Odd m ∧ Odd n := by simp [not_or, even_mul, ← not_even_iff_odd]
Product of Natural Numbers is Odd if and only if Both Factors are Odd
Informal description
For any natural numbers $m$ and $n$, the product $m \cdot n$ is odd if and only if both $m$ and $n$ are odd.
Nat.Odd.of_mul_left theorem
(h : Odd (m * n)) : Odd m
Full source 
lemma Odd.of_mul_left (h : Odd (m * n)) : Odd m :=
  (odd_mul.mp h).1
Oddness of Left Factor in Odd Product of Natural Numbers
Informal description
For any natural numbers $m$ and $n$, if the product $m \cdot n$ is odd, then $m$ is odd.
Nat.Odd.of_mul_right theorem
(h : Odd (m * n)) : Odd n
Full source 
lemma Odd.of_mul_right (h : Odd (m * n)) : Odd n :=
  (odd_mul.mp h).2
Oddness of Right Factor in Odd Product of Natural Numbers
Informal description
For any natural numbers $m$ and $n$, if the product $m \cdot n$ is odd, then $n$ is odd.
Nat.even_div theorem
: Even (m / n) ↔ m % (2 * n) / n = 0
Full source 
lemma even_div : EvenEven (m / n) ↔ m % (2 * n) / n = 0 := by
  rw [even_iff_two_dvd, dvd_iff_mod_eq_zero, ← Nat.mod_mul_right_div_self, mul_comm]
Characterization of Even Division via Remainder Condition
Informal description
For natural numbers $m$ and $n$, the division $m / n$ is even if and only if the remainder of $m$ divided by $2n$, further divided by $n$, equals zero. In other words, $\text{Even}(m / n) \leftrightarrow (m \bmod (2n)) / n = 0$.
Nat.odd_add theorem
: Odd (m + n) ↔ (Odd m ↔ Even n)
Full source 
@[parity_simps] lemma odd_add : OddOdd (m + n) ↔ (Odd m ↔ Even n) := by
  rw [← not_even_iff_odd, even_add, not_iff, ← not_even_iff_odd]
Odd Sum Characterization: $\text{Odd}(m + n) \leftrightarrow (\text{Odd}(m) \leftrightarrow \text{Even}(n))$
Informal description
For any natural numbers $m$ and $n$, the sum $m + n$ is odd if and only if $m$ is odd exactly when $n$ is even. In other words, $\text{Odd}(m + n) \leftrightarrow (\text{Odd}(m) \leftrightarrow \text{Even}(n))$.
Nat.odd_add' theorem
: Odd (m + n) ↔ (Odd n ↔ Even m)
Full source 
lemma odd_add' : OddOdd (m + n) ↔ (Odd n ↔ Even m) := by rw [add_comm, odd_add]
Odd Sum Characterization (Symmetric Form): $\text{Odd}(m + n) \leftrightarrow (\text{Odd}(n) \leftrightarrow \text{Even}(m))$
Informal description
For any natural numbers $m$ and $n$, the sum $m + n$ is odd if and only if $n$ is odd exactly when $m$ is even. In other words, $\text{Odd}(m + n) \leftrightarrow (\text{Odd}(n) \leftrightarrow \text{Even}(m))$.
Nat.ne_of_odd_add theorem
(h : Odd (m + n)) : m ≠ n
Full source 
lemma ne_of_odd_add (h : Odd (m + n)) : m ≠ n := by rintro rfl; simp [← not_even_iff_odd] at h
Non-equality of Summands for Odd Sum in Natural Numbers
Informal description
For any natural numbers $m$ and $n$, if the sum $m + n$ is odd, then $m$ is not equal to $n$.
Nat.odd_sub theorem
(h : n ≤ m) : Odd (m - n) ↔ (Odd m ↔ Even n)
Full source 
@[parity_simps] lemma odd_sub (h : n ≤ m) : OddOdd (m - n) ↔ (Odd m ↔ Even n) := by
  rw [← not_even_iff_odd, even_sub h, not_iff, ← not_even_iff_odd]
Odd Difference Characterization: $\text{Odd}(m - n) \leftrightarrow (\text{Odd}(m) \leftrightarrow \text{Even}(n))$ under $n \leq m$
Informal description
For any natural numbers $n$ and $m$ with $n \leq m$, the difference $m - n$ is odd if and only if $m$ is odd exactly when $n$ is even, i.e., $\text{Odd}(m - n) \leftrightarrow (\text{Odd}(m) \leftrightarrow \text{Even}(n))$.
Nat.Odd.sub_even theorem
(h : n ≤ m) (hm : Odd m) (hn : Even n) : Odd (m - n)
Full source 
lemma Odd.sub_even (h : n ≤ m) (hm : Odd m) (hn : Even n) : Odd (m - n) :=
  (odd_sub h).mpr <| iff_of_true hm hn
Odd Minus Even is Odd in Natural Numbers
Informal description
For any natural numbers $n$ and $m$ with $n \leq m$, if $m$ is odd and $n$ is even, then the difference $m - n$ is odd.
Nat.odd_sub' theorem
(h : n ≤ m) : Odd (m - n) ↔ (Odd n ↔ Even m)
Full source 
lemma odd_sub' (h : n ≤ m) : OddOdd (m - n) ↔ (Odd n ↔ Even m) := by
  rw [← not_even_iff_odd, even_sub h, not_iff, not_iff_comm, ← not_even_iff_odd]
Odd Difference Characterization: $\text{Odd}(m - n) \leftrightarrow (\text{Odd}(n) \leftrightarrow \text{Even}(m))$ under $n \leq m$
Informal description
For any natural numbers $n$ and $m$ with $n \leq m$, the difference $m - n$ is odd if and only if $n$ is odd exactly when $m$ is even, i.e., $\text{Odd}(m - n) \leftrightarrow (\text{Odd}(n) \leftrightarrow \text{Even}(m))$.
Nat.Even.sub_odd theorem
(h : n ≤ m) (hm : Even m) (hn : Odd n) : Odd (m - n)
Full source 
lemma Even.sub_odd (h : n ≤ m) (hm : Even m) (hn : Odd n) : Odd (m - n) :=
  (odd_sub' h).mpr <| iff_of_true hn hm
Odd Difference from Even Minus Odd Natural Numbers
Informal description
For any natural numbers $n$ and $m$ with $n \leq m$, if $m$ is even and $n$ is odd, then the difference $m - n$ is odd.
Nat.two_mul_div_two_add_one_of_odd theorem
(h : Odd n) : 2 * (n / 2) + 1 = n
Full source 
lemma two_mul_div_two_add_one_of_odd (h : Odd n) : 2 * (n / 2) + 1 = n := by
  rw [← odd_iff.mp h, div_add_mod]
Odd Natural Number Decomposition: $2 \cdot \lfloor n/2 \rfloor + 1 = n$
Informal description
For any odd natural number $n$, we have $2 \cdot \lfloor n/2 \rfloor + 1 = n$.
Nat.div_two_mul_two_add_one_of_odd theorem
(h : Odd n) : n / 2 * 2 + 1 = n
Full source 
lemma div_two_mul_two_add_one_of_odd (h : Odd n) : n / 2 * 2 + 1 = n := by
  rw [← odd_iff.mp h, div_add_mod']
Odd Natural Number Decomposition: $\left\lfloor \frac{n}{2} \right\rfloor \cdot 2 + 1 = n$
Informal description
For any odd natural number $n$, we have the decomposition $\left\lfloor \frac{n}{2} \right\rfloor \cdot 2 + 1 = n$.
Nat.one_add_div_two_mul_two_of_odd theorem
(h : Odd n) : 1 + n / 2 * 2 = n
Full source 
lemma one_add_div_two_mul_two_of_odd (h : Odd n) : 1 + n / 2 * 2 = n := by
  rw [← odd_iff.mp h, mod_add_div']
Odd natural number expressed as $1 + 2 \cdot \left\lfloor \frac{n}{2} \right\rfloor$
Informal description
For any odd natural number $n$, we have $1 + \left\lfloor \frac{n}{2} \right\rfloor \cdot 2 = n$.
Function.Involutive.iterate_bit0 theorem
(hf : Involutive f) (n : ℕ) : f^[2 * n] = id
Full source 
lemma iterate_bit0 (hf : Involutive f) (n : ℕ) : f^[2 * n] = id := by
  rw [iterate_mul, involutive_iff_iter_2_eq_id.1 hf, iterate_id]
Even Iteration of Involutive Function is Identity: $f^{[2n]} = \text{id}$
Informal description
For any involutive function $f \colon \alpha \to \alpha$ (i.e., $f(f(x)) = x$ for all $x \in \alpha$) and any natural number $n$, the $2n$-th iterate of $f$ equals the identity function, i.e., $f^{[2n]} = \text{id}$.
Function.Involutive.iterate_bit1 theorem
(hf : Involutive f) (n : ℕ) : f^[2 * n + 1] = f
Full source 
lemma iterate_bit1 (hf : Involutive f) (n : ℕ) : f^[2 * n + 1] = f := by
  rw [← succ_eq_add_one, iterate_succ, hf.iterate_bit0, id_comp]
Odd Iteration of Involutive Function Equals Original Function: $f^{[2n+1]} = f$
Informal description
For any involutive function $f \colon \alpha \to \alpha$ (i.e., $f(f(x)) = x$ for all $x \in \alpha$) and any natural number $n$, the $(2n+1)$-th iterate of $f$ equals $f$ itself, i.e., $f^{[2n+1]} = f$.
Function.Involutive.iterate_two_mul theorem
(hf : Involutive f) (n : ℕ) : f^[2 * n] = id
Full source 
lemma iterate_two_mul (hf : Involutive f) (n : ℕ) : f^[2 * n] = id := by
  rw [iterate_mul, involutive_iff_iter_2_eq_id.1 hf, iterate_id]
Even Iteration of Involutive Function is Identity: $f^{[2n]} = \mathrm{id}$
Informal description
For any involutive function $f \colon \alpha \to \alpha$ (i.e., satisfying $f(f(x)) = x$ for all $x \in \alpha$) and any natural number $n$, the $(2n)$-th iterate of $f$ equals the identity function, i.e., $f^{[2n]} = \mathrm{id}$.
Function.Involutive.iterate_even theorem
(hf : Involutive f) (hn : Even n) : f^[n] = id
Full source 
lemma iterate_even (hf : Involutive f) (hn : Even n) : f^[n] = id := by
  obtain ⟨m, rfl⟩ := hn
  rw [← two_mul, hf.iterate_two_mul]
Even Iteration of Involutive Function is Identity: $f^{[n]} = \mathrm{id}$ for even $n$
Informal description
For any involutive function $f \colon \alpha \to \alpha$ (i.e., satisfying $f(f(x)) = x$ for all $x \in \alpha$) and any even natural number $n$, the $n$-th iterate of $f$ equals the identity function, i.e., $f^{[n]} = \mathrm{id}$.
Function.Involutive.iterate_odd theorem
(hf : Involutive f) (hn : Odd n) : f^[n] = f
Full source 
lemma iterate_odd (hf : Involutive f) (hn : Odd n) : f^[n] = f := by
  obtain ⟨m, rfl⟩ := hn
  rw [iterate_add, hf.iterate_two_mul, id_comp, iterate_one]
Odd Iteration of Involutive Function: \( f^{[n]} = f \) for odd \( n \)
Informal description
For any involutive function \( f \colon \alpha \to \alpha \) (i.e., satisfying \( f(f(x)) = x \) for all \( x \in \alpha \)) and any odd natural number \( n \), the \( n \)-th iterate of \( f \) equals \( f \) itself, i.e., \( f^{[n]} = f \).
Function.Involutive.iterate_eq_self theorem
(hf : Involutive f) (hne : f ≠ id) : f^[n] = f ↔ Odd n
Full source 
lemma iterate_eq_self (hf : Involutive f) (hne : f ≠ id) : f^[n]f^[n] = f ↔ Odd n :=
  ⟨fun H ↦ not_even_iff_odd.1 fun hn ↦ hne <| by rwa [hf.iterate_even hn, eq_comm] at H,
    hf.iterate_odd⟩
Odd Iteration of Involutive Function Equals Itself: \( f^{[n]} = f \leftrightarrow \text{Odd } n \)
Informal description
For an involutive function \( f \colon \alpha \to \alpha \) (i.e., \( f(f(x)) = x \) for all \( x \in \alpha \)) that is not the identity function, the \( n \)-th iterate of \( f \) equals \( f \) itself if and only if \( n \) is an odd natural number. In other words, \( f^{[n]} = f \) if and only if \( n \) is odd.
Function.Involutive.iterate_eq_id theorem
(hf : Involutive f) (hne : f ≠ id) : f^[n] = id ↔ Even n
Full source 
lemma iterate_eq_id (hf : Involutive f) (hne : f ≠ id) : f^[n]f^[n] = id ↔ Even n :=
  ⟨fun H ↦ not_odd_iff_even.1 fun hn ↦ hne <| by rwa [hf.iterate_odd hn] at H, hf.iterate_even⟩
Characterization of Even Iteration of Involutive Function: \( f^{[n]} = \mathrm{id} \leftrightarrow \text{Even } n \)
Informal description
For an involutive function \( f \colon \alpha \to \alpha \) (i.e., satisfying \( f(f(x)) = x \) for all \( x \in \alpha \)) that is not the identity function, the \( n \)-th iterate of \( f \) equals the identity function if and only if \( n \) is an even natural number. In other words, \( f^{[n]} = \mathrm{id} \) if and only if \( n \) is even.
neg_one_pow_eq_ite theorem
: (-1 : R) ^ n = if Even n then 1 else (-1)
Full source 
lemma neg_one_pow_eq_ite : (-1 : R) ^ n = if Even n then 1 else (-1) := by
  cases even_or_odd n with
  | inl h => rw [h.neg_one_pow, if_pos h]
  | inr h => rw [h.neg_one_pow, if_neg (by simpa using h)]
Power of Negative One: $(-1)^n = 1$ if $n$ is even, $-1$ if $n$ is odd
Informal description
For any natural number $n$ and in any ring $R$, the $n$-th power of $-1$ equals $1$ if $n$ is even, and $-1$ if $n$ is odd. That is, \[ (-1)^n = \begin{cases} 1 & \text{if } n \text{ is even}, \\ -1 & \text{if } n \text{ is odd}. \end{cases} \]
neg_one_pow_congr theorem
(h : Even m ↔ Even n) : (-1 : R) ^ m = (-1) ^ n
Full source 
lemma neg_one_pow_congr (h : EvenEven m ↔ Even n) : (-1 : R) ^ m = (-1) ^ n := by
  simp [h, neg_one_pow_eq_ite]
Congruence of Powers of Negative One: $(-1)^m = (-1)^n$ under Evenness Condition
Informal description
For any natural numbers $m$ and $n$ in a ring $R$, if $m$ is even if and only if $n$ is even, then $(-1)^m = (-1)^n$.
neg_one_pow_eq_one_iff_even theorem
(h : (-1 : R) ≠ 1) : (-1 : R) ^ n = 1 ↔ Even n
Full source 
lemma neg_one_pow_eq_one_iff_even (h : (-1 : R) ≠ 1) :
    (-1 : R) ^ n = 1 ↔ Even n := by simp [neg_one_pow_eq_ite, h]
Characterization of Evenness via $(-1)^n = 1$ in Rings with $-1 \neq 1$
Informal description
Let $R$ be a ring with $-1 \neq 1$. For any natural number $n$, the power $(-1)^n$ equals $1$ if and only if $n$ is even. That is, \[ (-1)^n = 1 \leftrightarrow \text{$n$ is even}. \]
neg_one_pow_eq_neg_one_iff_odd theorem
(h : (-1 : R) ≠ 1) : (-1 : R) ^ n = -1 ↔ Odd n
Full source 
lemma neg_one_pow_eq_neg_one_iff_odd (h : (-1 : R) ≠ 1) :
    (-1 : R) ^ n = -1 ↔ Odd n := by simp [neg_one_pow_eq_ite, h.symm]
Power of Negative One Equals Negative One if and Only if Exponent is Odd
Informal description
For any natural number $n$ and any ring $R$ where $-1 \neq 1$, the $n$-th power of $-1$ equals $-1$ if and only if $n$ is odd. That is, \[ (-1)^n = -1 \leftrightarrow \text{$n$ is odd}. \]
natCast_eq_zero_of_even_of_two_eq_zero theorem
{n : ℕ} (hn : Even n) (h : (2 : R) = 0) : (n : R) = 0
Full source 
theorem natCast_eq_zero_of_even_of_two_eq_zero {n : ℕ} (hn : Even n) (h : (2 : R) = 0) :
    (n : R) = 0 :=
  (natCast_eq_zero_or_one_of_two_eq_zero' n h).1 hn
Even natural numbers map to zero when 2 equals zero in $R$
Informal description
For any natural number $n$ and any semiring $R$, if $n$ is even and $2 = 0$ in $R$, then the canonical image of $n$ in $R$ is zero, i.e., $(n : R) = 0$.
natCast_eq_one_of_odd_of_two_eq_zero theorem
{n : ℕ} (hn : Odd n) (h : (2 : R) = 0) : (n : R) = 1
Full source 
theorem natCast_eq_one_of_odd_of_two_eq_zero {n : ℕ} (hn : Odd n) (h : (2 : R) = 0) :
    (n : R) = 1 :=
  (natCast_eq_zero_or_one_of_two_eq_zero' n h).2 hn
Odd Natural Numbers Map to One in Rings Where Two Equals Zero
Informal description
For any natural number $n$ that is odd (i.e., $n = 2k + 1$ for some $k \in \mathbb{N}$), and for any ring $R$ where $2 = 0$, the canonical image of $n$ in $R$ is equal to $1$.
natCast_eq_zero_or_one_of_two_eq_zero theorem
(n : ℕ) (h : (2 : R) = 0) : (n : R) = 0 ∨ (n : R) = 1
Full source 
theorem natCast_eq_zero_or_one_of_two_eq_zero (n : ℕ) (h : (2 : R) = 0) :
    (n : R) = 0 ∨ (n : R) = 1 := by
  obtain hn | hn := Nat.even_or_odd n
  · exact Or.inl <| natCast_eq_zero_of_even_of_two_eq_zero hn h
  · exact Or.inr <| natCast_eq_one_of_odd_of_two_eq_zero hn h
Natural number images in characteristic 2 semirings are 0 or 1
Informal description
For any natural number $n$ and any semiring $R$ where $2 = 0$, the canonical image of $n$ in $R$ is either $0$ or $1$.