# 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 Algebra.Group.Even.

Algebra.Group.Even for the definition of even elements.

@[simp]
theorem Even.neg_pow {α : Type u_2} [] [] {n : } :
Even n∀ (a : α), (-a) ^ n = a ^ n
theorem Even.neg_one_pow {α : Type u_2} [] [] {n : } (h : Even n) :
(-1) ^ n = 1
theorem Even.neg_zpow {α : Type u_2} [] [] {n : } :
Even n∀ (a : α), (-a) ^ n = a ^ n
theorem Even.neg_one_zpow {α : Type u_2} [] [] {n : } (h : Even n) :
(-1) ^ n = 1
@[simp]
theorem isSquare_zero {α : Type u_2} [] :
theorem even_iff_exists_two_mul {α : Type u_2} [] {a : α} :
Even a ∃ (b : α), a = 2 * b
theorem even_iff_two_dvd {α : Type u_2} [] {a : α} :
Even a 2 a
theorem Even.two_dvd {α : Type u_2} [] {a : α} :
Even a2 a

Alias of the forward direction of even_iff_two_dvd.

theorem Even.trans_dvd {α : Type u_2} [] {a : α} {b : α} (ha : Even a) (hab : a b) :
theorem Dvd.dvd.even {α : Type u_2} [] {a : α} {b : α} (hab : a b) (ha : Even a) :
@[simp]
theorem range_two_mul (α : Type u_5) [] :
(Set.range fun (x : α) => 2 * x) = {a : α | Even a}
@[simp]
theorem even_bit0 {α : Type u_2} [] (a : α) :
@[simp]
theorem even_two {α : Type u_2} [] :
@[simp]
theorem Even.mul_left {α : Type u_2} [] {a : α} (ha : Even a) (b : α) :
Even (b * a)
@[simp]
theorem Even.mul_right {α : Type u_2} [] {a : α} (ha : Even a) (b : α) :
Even (a * b)
theorem even_two_mul {α : Type u_2} [] (a : α) :
Even (2 * a)
theorem Even.pow_of_ne_zero {α : Type u_2} [] {a : α} (ha : Even a) {n : } :
n 0Even (a ^ n)
def Odd {α : Type u_2} [] (a : α) :

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
theorem odd_iff_exists_bit1 {α : Type u_2} [] {a : α} :
Odd a ∃ (b : α), a = bit1 b
theorem Odd.exists_bit1 {α : Type u_2} [] {a : α} :
Odd a∃ (b : α), a = bit1 b

Alias of the forward direction of odd_iff_exists_bit1.

@[simp]
theorem odd_bit1 {α : Type u_2} [] (a : α) :
Odd (bit1 a)
@[simp]
theorem range_two_mul_add_one (α : Type u_5) [] :
(Set.range fun (x : α) => 2 * x + 1) = {a : α | Odd a}
theorem Even.add_odd {α : Type u_2} [] {a : α} {b : α} :
Even aOdd bOdd (a + b)
theorem Even.odd_add {α : Type u_2} [] {a : α} {b : α} (ha : Even a) (hb : Odd b) :
Odd (b + a)
theorem Odd.add_even {α : Type u_2} [] {a : α} {b : α} (ha : Odd a) (hb : Even b) :
Odd (a + b)
theorem Odd.add_odd {α : Type u_2} [] {a : α} {b : α} :
Odd aOdd bEven (a + b)
@[simp]
theorem odd_one {α : Type u_2} [] :
Odd 1
@[simp]
theorem Even.add_one {α : Type u_2} [] {a : α} (h : Even a) :
Odd (a + 1)
@[simp]
theorem Even.one_add {α : Type u_2} [] {a : α} (h : Even a) :
Odd (1 + a)
theorem odd_two_mul_add_one {α : Type u_2} [] (a : α) :
Odd (2 * a + 1)
@[simp]
theorem odd_add_self_one' {α : Type u_2} [] {a : α} :
Odd (a + (a + 1))
@[simp]
theorem odd_add_one_self {α : Type u_2} [] {a : α} :
Odd (a + 1 + a)
@[simp]
theorem odd_add_one_self' {α : Type u_2} [] {a : α} :
Odd (a + (1 + a))
theorem Odd.map {F : Type u_1} {α : Type u_2} {β : Type u_3} [] [] {a : α} [FunLike F α β] [RingHomClass F α β] (f : F) :
Odd aOdd (f a)
theorem Odd.natCast {R : Type u_5} [] {n : } (hn : Odd n) :
Odd n
@[simp]
theorem Odd.mul {α : Type u_2} [] {a : α} {b : α} :
Odd aOdd bOdd (a * b)
theorem Odd.pow {α : Type u_2} [] {a : α} (ha : Odd a) {n : } :
Odd (a ^ n)
theorem Odd.pow_add_pow_eq_zero {α : Type u_2} [] {a : α} {b : α} {n : } [] (hn : Odd n) (hab : a + b = 0) :
a ^ n + b ^ n = 0
theorem Odd.neg_pow {α : Type u_2} [] [] {n : } :
Odd n∀ (a : α), (-a) ^ n = -a ^ n
@[simp]
theorem Odd.neg_one_pow {α : Type u_2} [] [] {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)
theorem Nat.odd_iff {n : } :
Odd n n % 2 = 1
Equations
theorem Nat.not_odd_iff {n : } :
¬Odd n n % 2 = 0
@[simp]
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 : ) :
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.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 : ) :
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.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.bit0_div_two {n : } :
bit0 n / 2 = n
theorem Nat.bit1_div_two {n : } :
bit1 n / 2 = n
@[simp]
theorem Nat.bit0_div_bit0 {m : } {n : } :
bit0 n / bit0 m = n / m
@[simp]
theorem Nat.bit1_div_bit0 {m : } {n : } :
bit1 n / bit0 m = n / m
@[simp]
theorem Nat.bit0_mod_bit0 {m : } {n : } :
bit0 n % bit0 m = bit0 (n % m)
@[simp]
theorem Nat.bit1_mod_bit0 {m : } {n : } :
bit1 n % bit0 m = bit1 (n % m)
theorem Function.Involutive.iterate_bit0 {α : Type u_5} {f : αα} (hf : ) (n : ) :
f^[bit0 n] = id
theorem Function.Involutive.iterate_bit1 {α : Type u_5} {f : αα} (hf : ) (n : ) :
f^[bit1 n] = f
theorem Function.Involutive.iterate_two_mul {α : Type u_5} {f : αα} (hf : ) (n : ) :
f^[2 * n] = id
theorem Function.Involutive.iterate_even {α : Type u_5} {f : αα} {n : } (hf : ) (hn : Even n) :
f^[n] = id
theorem Function.Involutive.iterate_odd {α : Type u_5} {f : αα} {n : } (hf : ) (hn : Odd n) :
f^[n] = f
theorem Function.Involutive.iterate_eq_self {α : Type u_5} {f : αα} {n : } (hf : ) (hne : f id) :
f^[n] = f Odd n
theorem Function.Involutive.iterate_eq_id {α : Type u_5} {f : αα} {n : } (hf : ) (hne : f id) :
f^[n] = id Even n
theorem neg_one_pow_eq_one_iff_even {R : Type u_5} [] [] {n : } (h : -1 1) :
(-1) ^ n = 1 Even n