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.lean.

See also

Mathlib/Algebra/Group/Even.lean for the definition of even elements.

@[simp]

theorem Even.neg_pow {α : Type u_2} [Monoid α] [HasDistribNeg α] {n : ℕ} : Even n → ∀ (a : α), (-a) ^ n = a ^ n

theorem Even.neg_one_pow {α : Type u_2} [Monoid α] [HasDistribNeg α] {n : ℕ} (h : Even n) : (-1) ^ n = 1

@[simp]

theorem IsSquare.zero {α : Type u_2} [MulZeroClass α] : IsSquare 0

@[simp]

theorem even_two {α : Type u_2} [AddMonoidWithOne α] : Even 2

@[simp]

theorem Even.mul_left {α : Type u_2} [Add α] [Mul α] {a : α} [LeftDistribClass α] (ha : Even a) (b : α) : Even (b * a)

@[simp]

theorem Even.mul_right {α : Type u_2} [Add α] [Mul α] {a : α} [RightDistribClass α] (ha : Even a) (b : α) : Even (a * b)

theorem even_iff_exists_two_mul {α : Type u_2} [Semiring α] {a : α} : Even a ↔ ∃ (b : α), a = 2 * b

theorem even_iff_two_dvd {α : Type u_2} [Semiring α] {a : α} : Even a ↔ 2 ∣ a

theorem Even.two_dvd {α : Type u_2} [Semiring α] {a : α} : Even a → 2 ∣ a

Alias of the forward direction of even_iff_two_dvd.

theorem Even.trans_dvd {α : Type u_2} [Semiring α] {a b : α} (ha : Even a) (hab : a ∣ b) : Even b

theorem Dvd.dvd.even {α : Type u_2} [Semiring α] {a b : α} (hab : a ∣ b) (ha : Even a) : Even b

@[simp]

theorem range_two_mul (α : Type u_4) [NonAssocSemiring α] : (Set.range fun (x : α) => 2 * x) = {a : α | Even a}

theorem even_two_mul {α : Type u_2} [Semiring α] (a : α) : Even (2 * a)

theorem Even.pow_of_ne_zero {α : Type u_2} [Semiring α] {a : α} (ha : Even a) {n : ℕ} : n ≠ 0 → Even (a ^ n)

def Odd {α : Type u_2} [Semiring α] (a : α) : Prop

An element a of a semiring is odd if there exists k such a = 2*k + 1.

theorem odd_iff_exists_bit1 {α : Type u_2} [Semiring α] {a : α} : Odd a ↔ ∃ (b : α), a = 2 * b + 1

theorem Odd.exists_bit1 {α : Type u_2} [Semiring α] {a : α} : Odd a → ∃ (b : α), a = 2 * b + 1

Alias of the forward direction of odd_iff_exists_bit1.

@[simp]

theorem range_two_mul_add_one (α : Type u_4) [Semiring α] : (Set.range fun (x : α) => 2 * x + 1) = {a : α | Odd a}

theorem Even.add_odd {α : Type u_2} [Semiring α] {a b : α} : Even a → Odd b → Odd (a + b)

theorem Even.odd_add {α : Type u_2} [Semiring α] {a b : α} (ha : Even a) (hb : Odd b) : Odd (b + a)

theorem Odd.add_even {α : Type u_2} [Semiring α] {a b : α} (ha : Odd a) (hb : Even b) : Odd (a + b)

theorem Odd.add_odd {α : Type u_2} [Semiring α] {a b : α} : Odd a → Odd b → Even (a + b)

@[simp]

theorem odd_one {α : Type u_2} [Semiring α] : Odd 1

@[simp]

theorem Even.add_one {α : Type u_2} [Semiring α] {a : α} (h : Even a) : Odd (a + 1)

@[simp]

theorem Even.one_add {α : Type u_2} [Semiring α] {a : α} (h : Even a) : Odd (1 + a)

@[simp]

theorem Odd.add_one {α : Type u_2} [Semiring α] {a : α} (h : Odd a) : Even (a + 1)

@[simp]

theorem Odd.one_add {α : Type u_2} [Semiring α] {a : α} (h : Odd a) : Even (1 + a)

theorem odd_two_mul_add_one {α : Type u_2} [Semiring α] (a : α) : Odd (2 * a + 1)

@[simp]

theorem odd_add_self_one' {α : Type u_2} [Semiring α] {a : α} : Odd (a + (a + 1))

@[simp]

theorem odd_add_one_self {α : Type u_2} [Semiring α] {a : α} : Odd (a + 1 + a)

@[simp]

theorem odd_add_one_self' {α : Type u_2} [Semiring α] {a : α} : Odd (a + (1 + a))

theorem Odd.map {F : Type u_1} {α : Type u_2} {β : Type u_3} [Semiring α] [Semiring β] {a : α} [FunLike F α β] [RingHomClass F α β] (f : F) : Odd a → Odd (f a)

theorem Odd.natCast {R : Type u_4} [Semiring R] {n : ℕ} (hn : Odd n) : Odd ↑n

@[simp]

theorem Odd.mul {α : Type u_2} [Semiring α] {a b : α} : Odd a → Odd b → Odd (a * b)

theorem Odd.pow {α : Type u_2} [Semiring α] {a : α} {n : ℕ} (ha : Odd a) : Odd (a ^ n)

theorem Odd.pow_add_pow_eq_zero {α : Type u_2} [Semiring α] {a b : α} {n : ℕ} [IsCancelAdd α] (hn : Odd n) (hab : a + b = 0) : a ^ n + b ^ n = 0

theorem Even.of_isUnit_two {α : Type u_2} [Semiring α] (h : IsUnit 2) (a : α) : Even a

theorem isUnit_two_iff_forall_even {α : Type u_2} [Semiring α] : IsUnit 2 ↔ ∀ (a : α), Even a

theorem Odd.of_isUnit_two {α : Type u_2} [Ring α] (h : IsUnit 2) (a : α) : Odd a

theorem Odd.neg_pow {α : Type u_2} [Monoid α] [HasDistribNeg α] {n : ℕ} : Odd n → ∀ (a : α), (-a) ^ n = -a ^ n

@[simp]

theorem Odd.neg_one_pow {α : Type u_2} [Monoid α] [HasDistribNeg α] {n : ℕ} (h : Odd n) : (-1) ^ n = -1

theorem even_neg_two {α : Type u_2} [Ring α] : Even (-2)

theorem Odd.neg {α : Type u_2} [Ring α] {a : α} (hp : Odd a) : Odd (-a)

@[simp]

theorem odd_neg {α : Type u_2} [Ring α] {a : α} : Odd (-a) ↔ Odd a

theorem odd_neg_one {α : Type u_2} [Ring α] : Odd (-1)

theorem Odd.sub_even {α : Type u_2} [Ring α] {a b : α} (ha : Odd a) (hb : Even b) : Odd (a - b)

theorem Even.sub_odd {α : Type u_2} [Ring α] {a b : α} (ha : Even a) (hb : Odd b) : Odd (a - b)

theorem Odd.sub_odd {α : Type u_2} [Ring α] {a b : α} (ha : Odd a) (hb : Odd b) : Even (a - b)

@[simp]

theorem even_add_one {α : Type u_2} [Ring α] {a : α} : Even (a + 1) ↔ Odd a

@[simp]

theorem even_sub_one {α : Type u_2} [Ring α] {a : α} : Even (a - 1) ↔ Odd a

@[simp]

theorem even_add_two {α : Type u_2} [Ring α] {a : α} : Even (a + 2) ↔ Even a

@[simp]

theorem even_sub_two {α : Type u_2} [Ring α] {a : α} : Even (a - 2) ↔ Even a

@[simp]

theorem odd_add_one {α : Type u_2} [Ring α] {a : α} : Odd (a + 1) ↔ Even a

@[simp]

theorem odd_sub_one {α : Type u_2} [Ring α] {a : α} : Odd (a - 1) ↔ Even a

@[simp]

theorem odd_add_two {α : Type u_2} [Ring α] {a : α} : Odd (a + 2) ↔ Odd a

@[simp]

theorem odd_sub_two {α : Type u_2} [Ring α] {a : α} : Odd (a - 2) ↔ Odd a

theorem Nat.odd_iff {n : ℕ} : Odd n ↔ n % 2 = 1

@[implicit_reducible]

instance Nat.instDecidablePredOdd : DecidablePred Odd

theorem Nat.not_odd_iff {n : ℕ} : ¬Odd n ↔ n % 2 = 0

@[simp]

theorem Nat.not_odd_iff_even {n : ℕ} : ¬Odd n ↔ Even n

@[simp]

theorem Nat.not_even_iff_odd {n : ℕ} : ¬Even n ↔ Odd n

@[simp]

theorem Nat.not_odd_zero : ¬Odd 0

theorem Odd.not_two_dvd_nat {n : ℕ} (h : Odd n) : ¬2 ∣ n

theorem Nat.even_xor_odd (n : ℕ) : Xor' (Even n) (Odd n)

theorem Nat.even_or_odd (n : ℕ) : Even n ∨ Odd n

theorem Nat.even_or_odd' (n : ℕ) : ∃ (k : ℕ), n = 2 * k ∨ n = 2 * k + 1

theorem Nat.even_xor_odd' (n : ℕ) : ∃ (k : ℕ), Xor' (n = 2 * k) (n = 2 * k + 1)

theorem Nat.odd_add_one {n : ℕ} : Odd (n + 1) ↔ ¬Odd n

theorem Nat.mod_two_add_add_odd_mod_two (m : ℕ) {n : ℕ} (hn : Odd n) : m % 2 + (m + n) % 2 = 1

@[simp]

theorem Nat.mod_two_add_succ_mod_two (m : ℕ) : m % 2 + (m + 1) % 2 = 1

@[simp]

theorem Nat.succ_mod_two_add_mod_two (m : ℕ) : (m + 1) % 2 + m % 2 = 1

theorem Nat.even_add' {m n : ℕ} : Even (m + n) ↔ (Odd m ↔ Odd n)

@[simp]

theorem Nat.not_even_bit1 (n : ℕ) : ¬Even (2 * n + 1)

theorem Nat.not_even_two_mul_add_one (n : ℕ) : ¬Even (2 * n + 1)

theorem Nat.even_sub' {m n : ℕ} (h : n ≤ m) : Even (m - n) ↔ (Odd m ↔ Odd n)

theorem Nat.Odd.sub_odd {m n : ℕ} (hm : Odd m) (hn : Odd n) : Even (m - n)

theorem Odd.tsub_odd {m n : ℕ} (hm : Odd m) (hn : Odd n) : Even (m - n)

Alias of Nat.Odd.sub_odd.

theorem Nat.odd_mul {m n : ℕ} : Odd (m * n) ↔ Odd m ∧ Odd n

theorem Nat.Odd.of_mul_left {m n : ℕ} (h : Odd (m * n)) : Odd m

theorem Nat.Odd.of_mul_right {m n : ℕ} (h : Odd (m * n)) : Odd n

theorem Nat.odd_pow_iff {n e : ℕ} (he : e ≠ 0) : Odd (n ^ e) ↔ Odd n

theorem Nat.even_div {m n : ℕ} : Even (m / n) ↔ m % (2 * n) / n = 0

theorem Nat.odd_add {m n : ℕ} : Odd (m + n) ↔ (Odd m ↔ Even n)

theorem Nat.odd_add' {m n : ℕ} : Odd (m + n) ↔ (Odd n ↔ Even m)

theorem Nat.ne_of_odd_add {m n : ℕ} (h : Odd (m + n)) : m ≠ n

theorem Nat.odd_sub {m n : ℕ} (h : n ≤ m) : Odd (m - n) ↔ (Odd m ↔ Even n)

theorem Nat.Odd.sub_even {m n : ℕ} (h : n ≤ m) (hm : Odd m) (hn : Even n) : Odd (m - n)

theorem Nat.odd_sub' {m n : ℕ} (h : n ≤ m) : Odd (m - n) ↔ (Odd n ↔ Even m)

theorem Nat.Even.sub_odd {m n : ℕ} (h : n ≤ m) (hm : Even m) (hn : Odd n) : Odd (m - n)

theorem Nat.two_mul_div_two_add_one_of_odd {n : ℕ} (h : Odd n) : 2 * (n / 2) + 1 = n

theorem Nat.div_two_mul_two_add_one_of_odd {n : ℕ} (h : Odd n) : n / 2 * 2 + 1 = n

theorem Nat.one_add_div_two_mul_two_of_odd {n : ℕ} (h : Odd n) : 1 + n / 2 * 2 = n

theorem Nat.two_dvd_mul_add_one (k : ℕ) : 2 ∣ k * (k + 1)

theorem Nat.two_dvd_mul_sub_one (k : ℕ) : 2 ∣ k * (k - 1)

theorem Function.Involutive.iterate_two_mul {α : Type u_4} {f : α → α} (hf : Involutive f) (n : ℕ) : f^[2 * n] = id

@[deprecated Function.Involutive.iterate_two_mul (since := "2025-10-28")]

theorem Function.Involutive.iterate_bit0 {α : Type u_4} {f : α → α} (hf : Involutive f) (n : ℕ) : f^[2 * n] = id

Alias of Function.Involutive.iterate_two_mul.

theorem Function.Involutive.iterate_two_mul_add_one {α : Type u_4} {f : α → α} (hf : Involutive f) (n : ℕ) : f^[2 * n + 1] = f

@[deprecated Function.Involutive.iterate_two_mul_add_one (since := "2025-10-28")]

theorem Function.Involutive.iterate_bit1 {α : Type u_4} {f : α → α} (hf : Involutive f) (n : ℕ) : f^[2 * n + 1] = f

Alias of Function.Involutive.iterate_two_mul_add_one.

theorem Function.Involutive.iterate_even {α : Type u_4} {f : α → α} {n : ℕ} (hf : Involutive f) (hn : Even n) : f^[n] = id

theorem Function.Involutive.iterate_odd {α : Type u_4} {f : α → α} {n : ℕ} (hf : Involutive f) (hn : Odd n) : f^[n] = f

theorem Function.Involutive.iterate_eq_self {α : Type u_4} {f : α → α} {n : ℕ} (hf : Involutive f) (hne : f ≠ id) : f^[n] = f ↔ Odd n

theorem Function.Involutive.iterate_eq_id {α : Type u_4} {f : α → α} {n : ℕ} (hf : Involutive f) (hne : f ≠ id) : f^[n] = id ↔ Even n

theorem neg_one_pow_eq_ite {R : Type u_4} [Monoid R] [HasDistribNeg R] {n : ℕ} : (-1) ^ n = if Even n then 1 else -1

theorem neg_one_pow_congr {R : Type u_4} [Monoid R] [HasDistribNeg R] {m n : ℕ} (h : Even m ↔ Even n) : (-1) ^ m = (-1) ^ n

theorem neg_one_pow_eq_one_iff_even {R : Type u_4} [Monoid R] [HasDistribNeg R] {n : ℕ} (h : -1 ≠ 1) : (-1) ^ n = 1 ↔ Even n

theorem neg_one_pow_eq_neg_one_iff_odd {R : Type u_4} [Monoid R] [HasDistribNeg R] {n : ℕ} (h : -1 ≠ 1) : (-1) ^ n = -1 ↔ Odd n

theorem Even.neg_zpow {α : Type u_2} [DivisionMonoid α] [HasDistribNeg α] {n : ℤ} : Even n → ∀ (a : α), (-a) ^ n = a ^ n

theorem Even.neg_one_zpow {α : Type u_2} [DivisionMonoid α] [HasDistribNeg α] {n : ℤ} (h : Even n) : (-1) ^ n = 1

theorem neg_one_zpow_eq_ite {α : Type u_2} [DivisionMonoid α] [HasDistribNeg α] {n : ℤ} : (-1) ^ n = if Even n then 1 else -1

theorem natCast_eq_zero_of_even_of_two_eq_zero {R : Type u_4} [AddMonoidWithOne R] {n : ℕ} (hn : Even n) (h : 2 = 0) : ↑n = 0

theorem natCast_eq_one_of_odd_of_two_eq_zero {R : Type u_4} [AddMonoidWithOne R] {n : ℕ} (hn : Odd n) (h : 2 = 0) : ↑n = 1

theorem natCast_eq_zero_or_one_of_two_eq_zero {R : Type u_4} [AddMonoidWithOne R] (n : ℕ) (h : 2 = 0) : ↑n = 0 ∨ ↑n = 1