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.

See also

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

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

@[simp]

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

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_5) [Semiring α] : (Set.range fun (x : α) => 2 * x) = {a : α | Even a}

@[simp]

theorem even_bit0 {α : Type u_2} [Semiring α] (a : α) : Even (bit0 a)

@[simp]

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

@[simp]

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

@[simp]

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

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.

Equations

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

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

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

Alias of the forward direction of odd_iff_exists_bit1.

@[simp]

theorem odd_bit1 {α : Type u_2} [Semiring α] (a : α) : Odd (bit1 a)

@[simp]

theorem range_two_mul_add_one (α : Type u_5) [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)

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_5} [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 : α} (ha : Odd a) {n : ℕ} : 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 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)

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

instance Nat.instDecidablePredOdd : DecidablePred Odd

Equations

• x.instDecidablePredOdd = decidable_of_iff (x % 2 = 1) ⋯

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

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

@[simp]

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

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.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 (bit1 n)

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.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 : Function.Involutive f) (n : ℕ) : f^[bit0 n] = id

theorem Function.Involutive.iterate_bit1 {α : Type u_5} {f : α → α} (hf : Function.Involutive f) (n : ℕ) : f^[bit1 n] = f

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

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

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

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

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

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