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

source
@[simp]
theorem Even.neg_pow {α : Type u_2} [Monoid α] [HasDistribNeg α] {n : ℕ} :
Even n → ∀ (a : α), (-a) ^ n = a ^ n
source
theorem Even.neg_one_pow {α : Type u_2} [Monoid α] [HasDistribNeg α] {n : ℕ} (h : Even n) :
(-1) ^ n = 1
source
theorem Even.neg_zpow {α : Type u_2} [DivisionMonoid α] [HasDistribNeg α] {n : ℤ} :
Even n → ∀ (a : α), (-a) ^ n = a ^ n
source
theorem Even.neg_one_zpow {α : Type u_2} [DivisionMonoid α] [HasDistribNeg α] {n : ℤ} (h : Even n) :
(-1) ^ n = 1
source
@[simp]
theorem IsSquare.zero {α : Type u_2} [MulZeroClass α] :
IsSquare 0
source
theorem even_iff_exists_two_mul {α : Type u_2} [Semiring α] {a : α} :
Even a ↔ ∃ (b : α), a = 2 * b
source
theorem even_iff_two_dvd {α : Type u_2} [Semiring α] {a : α} :
Even a ↔ 2 ∣ a
source
theorem Even.two_dvd {α : Type u_2} [Semiring α] {a : α} :
Even a → 2 ∣ a

Alias of the forward direction of `even_iff_two_dvd`.

source
theorem Even.trans_dvd {α : Type u_2} [Semiring α] {a b : α} (ha : Even a) (hab : a ∣ b) :
Even b
source
theorem Dvd.dvd.even {α : Type u_2} [Semiring α] {a b : α} (hab : a ∣ b) (ha : Even a) :
Even b
source
@[simp]
theorem range_two_mul (α : Type u_4) [NonAssocSemiring α] :
(Set.range fun (x : α) => 2 * x) = {a : α | Even a}
source
@[simp]
theorem even_two {α : Type u_2} [Semiring α] :
Even 2
source
@[simp]
theorem Even.mul_left {α : Type u_2} [Semiring α] {a : α} (ha : Even a) (b : α) :
Even (b * a)
source
@[simp]
theorem Even.mul_right {α : Type u_2} [Semiring α] {a : α} (ha : Even a) (b : α) :
Even (a * b)
source
theorem even_two_mul {α : Type u_2} [Semiring α] (a : α) :
Even (2 * a)
source
theorem Even.pow_of_ne_zero {α : Type u_2} [Semiring α] {a : α} (ha : Even a) {n : ℕ} :
n ≠ 0 → Even (a ^ n)
source
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`.

Equations

- Odd a = ∃ (k : α), a = 2 * k + 1

Instances For

source
theorem odd_iff_exists_bit1 {α : Type u_2} [Semiring α] {a : α} :
Odd a ↔ ∃ (b : α), a = 2 * b + 1
source
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`.

source
@[simp]
theorem range_two_mul_add_one (α : Type u_4) [Semiring α] :
(Set.range fun (x : α) => 2 * x + 1) = {a : α | Odd a}
source
theorem Even.add_odd {α : Type u_2} [Semiring α] {a b : α} :
Even a → Odd b → Odd (a + b)
source
theorem Even.odd_add {α : Type u_2} [Semiring α] {a b : α} (ha : Even a) (hb : Odd b) :
Odd (b + a)
source
theorem Odd.add_even {α : Type u_2} [Semiring α] {a b : α} (ha : Odd a) (hb : Even b) :
Odd (a + b)
source
theorem Odd.add_odd {α : Type u_2} [Semiring α] {a b : α} :
Odd a → Odd b → Even (a + b)
source
@[simp]
theorem odd_one {α : Type u_2} [Semiring α] :
Odd 1
source
@[simp]
theorem Even.add_one {α : Type u_2} [Semiring α] {a : α} (h : Even a) :
Odd (a + 1)
source
@[simp]
theorem Even.one_add {α : Type u_2} [Semiring α] {a : α} (h : Even a) :
Odd (1 + a)
source
@[simp]
theorem Odd.add_one {α : Type u_2} [Semiring α] {a : α} (h : Odd a) :
Even (a + 1)
source
@[simp]
theorem Odd.one_add {α : Type u_2} [Semiring α] {a : α} (h : Odd a) :
Even (1 + a)
source
theorem odd_two_mul_add_one {α : Type u_2} [Semiring α] (a : α) :
Odd (2 * a + 1)
source
@[simp]
theorem odd_add_self_one' {α : Type u_2} [Semiring α] {a : α} :
Odd (a + (a + 1))
source
@[simp]
theorem odd_add_one_self {α : Type u_2} [Semiring α] {a : α} :
Odd (a + 1 + a)
source
@[simp]
theorem odd_add_one_self' {α : Type u_2} [Semiring α] {a : α} :
Odd (a + (1 + a))
source
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)
source
theorem Odd.natCast {R : Type u_4} [Semiring R] {n : ℕ} (hn : Odd n) :
Odd ↑n
source
@[simp]
theorem Odd.mul {α : Type u_2} [Semiring α] {a b : α} :
Odd a → Odd b → Odd (a * b)
source
theorem Odd.pow {α : Type u_2} [Semiring α] {a : α} {n : ℕ} (ha : Odd a) :
Odd (a ^ n)
source
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
source
theorem Even.of_isUnit_two {α : Type u_2} [Semiring α] (h : IsUnit 2) (a : α) :
Even a
source
theorem isUnit_two_iff_forall_even {α : Type u_2} [Semiring α] :
IsUnit 2 ↔ ∀ (a : α), Even a
source
theorem Odd.of_isUnit_two {α : Type u_2} [Ring α] (h : IsUnit 2) (a : α) :
Odd a
source
theorem Odd.neg_pow {α : Type u_2} [Monoid α] [HasDistribNeg α] {n : ℕ} :
Odd n → ∀ (a : α), (-a) ^ n = -a ^ n
source
@[simp]
theorem Odd.neg_one_pow {α : Type u_2} [Monoid α] [HasDistribNeg α] {n : ℕ} (h : Odd n) :
(-1) ^ n = -1
source
theorem even_neg_two {α : Type u_2} [Ring α] :
Even (-2)
source
theorem Odd.neg {α : Type u_2} [Ring α] {a : α} (hp : Odd a) :
Odd (-a)
source
@[simp]
theorem odd_neg {α : Type u_2} [Ring α] {a : α} :
Odd (-a) ↔ Odd a
source
theorem odd_neg_one {α : Type u_2} [Ring α] :
Odd (-1)
source
theorem Odd.sub_even {α : Type u_2} [Ring α] {a b : α} (ha : Odd a) (hb : Even b) :
Odd (a - b)
source
theorem Even.sub_odd {α : Type u_2} [Ring α] {a b : α} (ha : Even a) (hb : Odd b) :
Odd (a - b)
source
theorem Odd.sub_odd {α : Type u_2} [Ring α] {a b : α} (ha : Odd a) (hb : Odd b) :
Even (a - b)
source
theorem Nat.odd_iff {n : ℕ} :
Odd n ↔ n % 2 = 1
source
instance Nat.instDecidablePredOdd :
DecidablePred Odd
Equations

- x✝.instDecidablePredOdd = decidable_of_iff (x✝ % 2 = 1) ⋯

source
theorem Nat.not_odd_iff {n : ℕ} :
¬Odd n ↔ n % 2 = 0
source
@[simp]
theorem Nat.not_odd_iff_even {n : ℕ} :
¬Odd n ↔ Even n
source
@[simp]
theorem Nat.not_even_iff_odd {n : ℕ} :
¬Even n ↔ Odd n
source
@[simp]
theorem Nat.not_odd_zero :
¬Odd 0
source
theorem Odd.not_two_dvd_nat {n : ℕ} (h : Odd n) :
¬2 ∣ n
source
theorem Nat.even_xor_odd (n : ℕ) :
Xor' (Even n) (Odd n)
source
theorem Nat.even_or_odd (n : ℕ) :
Even n ∨ Odd n
source
theorem Nat.even_or_odd' (n : ℕ) :
∃ (k : ℕ), n = 2 * k ∨ n = 2 * k + 1
source
theorem Nat.even_xor_odd' (n : ℕ) :
∃ (k : ℕ), Xor' (n = 2 * k) (n = 2 * k + 1)
source
theorem Nat.odd_add_one {n : ℕ} :
Odd (n + 1) ↔ ¬Odd n
source
theorem Nat.mod_two_add_add_odd_mod_two (m : ℕ) {n : ℕ} (hn : Odd n) :
m % 2 + (m + n) % 2 = 1
source
@[simp]
theorem Nat.mod_two_add_succ_mod_two (m : ℕ) :
m % 2 + (m + 1) % 2 = 1
source
@[simp]
theorem Nat.succ_mod_two_add_mod_two (m : ℕ) :
(m + 1) % 2 + m % 2 = 1
source
theorem Nat.even_add' {m n : ℕ} :
Even (m + n) ↔ (Odd m ↔ Odd n)
source
@[simp]
theorem Nat.not_even_bit1 (n : ℕ) :
¬Even (2 * n + 1)
source
theorem Nat.not_even_two_mul_add_one (n : ℕ) :
¬Even (2 * n + 1)
source
theorem Nat.even_sub' {m n : ℕ} (h : n ≤ m) :
Even (m - n) ↔ (Odd m ↔ Odd n)
source
theorem Nat.Odd.sub_odd {m n : ℕ} (hm : Odd m) (hn : Odd n) :
Even (m - n)
source
theorem Odd.tsub_odd {m n : ℕ} (hm : Odd m) (hn : Odd n) :
Even (m - n)

Alias of `Nat.Odd.sub_odd`.

source
theorem Nat.odd_mul {m n : ℕ} :
Odd (m * n) ↔ Odd m ∧ Odd n
source
theorem Nat.Odd.of_mul_left {m n : ℕ} (h : Odd (m * n)) :
Odd m
source
theorem Nat.Odd.of_mul_right {m n : ℕ} (h : Odd (m * n)) :
Odd n
source
theorem Nat.odd_pow_iff {n e : ℕ} (he : e ≠ 0) :
Odd (n ^ e) ↔ Odd n
source
theorem Nat.even_div {m n : ℕ} :
Even (m / n) ↔ m % (2 * n) / n = 0
source
theorem Nat.odd_add {m n : ℕ} :
Odd (m + n) ↔ (Odd m ↔ Even n)
source
theorem Nat.odd_add' {m n : ℕ} :
Odd (m + n) ↔ (Odd n ↔ Even m)
source
theorem Nat.ne_of_odd_add {m n : ℕ} (h : Odd (m + n)) :
m ≠ n
source
theorem Nat.odd_sub {m n : ℕ} (h : n ≤ m) :
Odd (m - n) ↔ (Odd m ↔ Even n)
source
theorem Nat.Odd.sub_even {m n : ℕ} (h : n ≤ m) (hm : Odd m) (hn : Even n) :
Odd (m - n)
source
theorem Nat.odd_sub' {m n : ℕ} (h : n ≤ m) :
Odd (m - n) ↔ (Odd n ↔ Even m)
source
theorem Nat.Even.sub_odd {m n : ℕ} (h : n ≤ m) (hm : Even m) (hn : Odd n) :
Odd (m - n)
source
theorem Nat.two_mul_div_two_add_one_of_odd {n : ℕ} (h : Odd n) :
2 * (n / 2) + 1 = n
source
theorem Nat.div_two_mul_two_add_one_of_odd {n : ℕ} (h : Odd n) :
n / 2 * 2 + 1 = n
source
theorem Nat.one_add_div_two_mul_two_of_odd {n : ℕ} (h : Odd n) :
1 + n / 2 * 2 = n
source
theorem Nat.two_dvd_mul_add_one (k : ℕ) :
2 ∣ k * (k + 1)
source
theorem Function.Involutive.iterate_two_mul {α : Type u_4} {f : α → α} (hf : Involutive f) (n : ℕ) :
f^[2 * n] = id
source
@[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`.

source
theorem Function.Involutive.iterate_two_mul_add_one {α : Type u_4} {f : α → α} (hf : Involutive f) (n : ℕ) :
f^[2 * n + 1] = f
source
@[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`.

source
theorem Function.Involutive.iterate_even {α : Type u_4} {f : α → α} {n : ℕ} (hf : Involutive f) (hn : Even n) :
f^[n] = id
source
theorem Function.Involutive.iterate_odd {α : Type u_4} {f : α → α} {n : ℕ} (hf : Involutive f) (hn : Odd n) :
f^[n] = f
source
theorem Function.Involutive.iterate_eq_self {α : Type u_4} {f : α → α} {n : ℕ} (hf : Involutive f) (hne : f ≠ id) :
f^[n] = f ↔ Odd n
source
theorem Function.Involutive.iterate_eq_id {α : Type u_4} {f : α → α} {n : ℕ} (hf : Involutive f) (hne : f ≠ id) :
f^[n] = id ↔ Even n
source
theorem neg_one_pow_eq_ite {R : Type u_4} [Monoid R] [HasDistribNeg R] {n : ℕ} :
(-1) ^ n = if Even n then 1 else -1
source
theorem neg_one_pow_congr {R : Type u_4} [Monoid R] [HasDistribNeg R] {m n : ℕ} (h : Even m ↔ Even n) :
(-1) ^ m = (-1) ^ n
source
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
source
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
source
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
source
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
source
theorem natCast_eq_zero_or_one_of_two_eq_zero {R : Type u_4} [AddMonoidWithOne R] (n : ℕ) (h : 2 = 0) :
↑n = 0 ∨ ↑n = 1