algebra.parity

# Squares, even and odd elements #

THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.

This file proves some general facts about squares, even and odd elements of semirings.

In the implementation, we define is_square and we let even be the notion transported by to_additive. The definition are therefore as follows:

is_square a ↔ ∃ r, a = r * r
even a ↔ ∃ r, a = r + r


Odd elements are not unified with a multiplicative notion.

## Future work #

• TODO: Try to generalize further the typeclass assumptions on is_square/even. For instance, in some cases, there are semiring assumptions that I (DT) am not convinced are necessary.
• TODO: Consider moving the definition and lemmas about odd to a separate file.
• TODO: The "old" definition of even a asked for the existence of an element c such that a = 2 * c. For this reason, several fixes introduce an extra two_mul or ← two_mul. It might be the case that by making a careful choice of simp lemma, this can be avoided.
def is_square {α : Type u_2} [has_mul α] (a : α) :
Prop

An element a of a type α with multiplication satisfies is_square a if a = r * r, for some r : α.

Equations
Instances for is_square
def even {α : Type u_2} [has_add α] (a : α) :
Prop

An element a of a type α with addition satisfies even a if a = r + r, for some r : α.

Equations
Instances for even
@[simp]
theorem even_add_self {α : Type u_2} [has_add α] (m : α) :
even (m + m)
@[simp]
theorem is_square_mul_self {α : Type u_2} [has_mul α] (m : α) :
is_square (m * m)
theorem even_op_iff {α : Type u_2} [has_add α] (a : α) :
theorem is_square_op_iff {α : Type u_2} [has_mul α] (a : α) :
@[simp]
theorem even_zero {α : Type u_2}  :
@[simp]
theorem is_square_one {α : Type u_2}  :
theorem is_square.map {F : Type u_1} {α : Type u_2} {β : Type u_3} [ β] {m : α} (f : F) :
theorem even.map {F : Type u_1} {α : Type u_2} {β : Type u_3} [ β] {m : α} (f : F) :
even m even (f m)
theorem even_iff_exists_two_nsmul {α : Type u_2} [add_monoid α] (m : α) :
even m (c : α), m = 2 c
theorem is_square_iff_exists_sq {α : Type u_2} [monoid α] (m : α) :
(c : α), m = c ^ 2
theorem is_square_of_exists_sq {α : Type u_2} [monoid α] (m : α) :
( (c : α), m = c ^ 2)

Alias of the reverse direction of is_square_iff_exists_sq.

theorem is_square.exists_sq {α : Type u_2} [monoid α] (m : α) :
( (c : α), m = c ^ 2)

Alias of the forward direction of is_square_iff_exists_sq.

theorem even.exists_two_nsmul {α : Type u_2} [add_monoid α] (m : α) :
even m ( (c : α), m = 2 c)

Alias of the forwards direction of even_iff_exists_two_nsmul.

theorem even_of_exists_two_nsmul {α : Type u_2} [add_monoid α] (m : α) :
( (c : α), m = 2 c) even m

Alias of the backwards direction of even_iff_exists_two_nsmul.

theorem even.nsmul {α : Type u_2} [add_monoid α] {a : α} (n : ) :
even a even (n a)
theorem is_square.pow {α : Type u_2} [monoid α] {a : α} (n : ) :
is_square (a ^ n)
@[simp]
theorem even.nsmul' {α : Type u_2} [add_monoid α] {n : } :
even n (a : α), even (n a)
@[simp]
theorem even.is_square_pow {α : Type u_2} [monoid α] {n : } :
even n (a : α), is_square (a ^ n)
@[simp]
theorem even_two_nsmul {α : Type u_2} [add_monoid α] (a : α) :
even (2 a)
@[simp]
theorem is_square_sq {α : Type u_2} [monoid α] (a : α) :
is_square (a ^ 2)
theorem even.neg_pow {α : Type u_2} [monoid α] {n : }  :
even n (a : α), (-a) ^ n = a ^ n
theorem even.neg_one_pow {α : Type u_2} [monoid α] {n : } (h : even n) :
(-1) ^ n = 1
theorem is_square.mul {α : Type u_2} {a b : α} :
theorem even.add {α : Type u_2} {a b : α} :
even a even b even (a + b)
@[simp]
theorem is_square_zero (α : Type u_2)  :
@[simp]
theorem even_neg {α : Type u_2} {a : α} :
even (-a) even a
@[simp]
theorem is_square_inv {α : Type u_2} {a : α} :
theorem is_square.inv {α : Type u_2} {a : α} :

Alias of the reverse direction of is_square_inv.

theorem even.neg {α : Type u_2} {a : α} :
even a even (-a)

Alias of the reverse direction of is_square_inv.

theorem even.zsmul {α : Type u_2} {a : α} (n : ) :
even a even (n a)
theorem is_square.zpow {α : Type u_2} {a : α} (n : ) :
is_square (a ^ n)
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
theorem even_abs {α : Type u_2} [linear_order α] {a : α} :
theorem is_square.div {α : Type u_2} {a b : α} (ha : is_square a) (hb : is_square b) :
is_square (a / b)
theorem even.sub {α : Type u_2} {a b : α} (ha : even a) (hb : even b) :
even (a - b)
@[simp]
theorem even.zsmul' {α : Type u_2} [add_group α] {n : } :
even n (a : α), even (n a)
@[simp]
theorem even.is_square_zpow {α : Type u_2} [group α] {n : } :
even n (a : α), is_square (a ^ n)
theorem even.tsub {α : Type u_2} [has_sub α] {m n : α} (hm : even m) (hn : even n) :
even (m - n)
theorem even_iff_exists_bit0 {α : Type u_2} [has_add α] {a : α} :
even a (b : α), a = bit0 b
theorem even.exists_bit0 {α : Type u_2} [has_add α] {a : α} :
even a ( (b : α), a = bit0 b)

Alias of the forward direction of even_iff_exists_bit0.

theorem even_iff_exists_two_mul {α : Type u_2} [semiring α] (m : α) :
even m (c : α), m = 2 * c
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 α] {m n : α} (hm : even m) (hn : m n) :
theorem has_dvd.dvd.even {α : Type u_2} [semiring α] {m n : α} (hn : m n) (hm : even m) :
@[simp]
theorem range_two_mul (α : Type u_1) [semiring α] :
set.range (λ (x : α), 2 * x) = {a : α | even a}
@[simp]
theorem even_bit0 {α : Type u_2} [semiring α] (a : α) :
@[simp]
theorem even_two {α : Type u_2} [semiring α] :
@[simp]
theorem even.mul_left {α : Type u_2} [semiring α] {m : α} (hm : even m) (n : α) :
even (n * m)
@[simp]
theorem even.mul_right {α : Type u_2} [semiring α] {m : α} (hm : even m) (n : α) :
even (m * n)
theorem even_two_mul {α : Type u_2} [semiring α] (m : α) :
even (2 * m)
theorem even.pow_of_ne_zero {α : Type u_2} [semiring α] {m : α} (hm : even m) {a : } :
a 0 even (m ^ a)
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
Instances for odd
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_1) [semiring α] :
set.range (λ (x : α), 2 * x + 1) = {a : α | odd a}
theorem even.add_odd {α : Type u_2} [semiring α] {m n : α} :
even m odd n odd (m + n)
theorem odd.add_even {α : Type u_2} [semiring α] {m n : α} (hm : odd m) (hn : even n) :
odd (m + n)
theorem odd.add_odd {α : Type u_2} [semiring α] {m n : α} :
odd m odd n even (m + n)
@[simp]
theorem odd_one {α : Type u_2} [semiring α] :
odd 1
@[simp]
theorem odd_two_mul_add_one {α : Type u_2} [semiring α] (m : α) :
odd (2 * m + 1)
theorem odd.map {F : Type u_1} {α : Type u_2} {β : Type u_3} [semiring α] [semiring β] {m : α} [ β] (f : F) :
odd m odd (f m)
@[simp]
theorem odd.mul {α : Type u_2} [semiring α] {m n : α} :
odd m odd n odd (m * n)
theorem odd.pow {α : Type u_2} [semiring α] {m : α} (hm : odd m) {a : } :
odd (m ^ a)
theorem odd.neg_pow {α : Type u_2} [monoid α] {n : } :
odd n (a : α), (-a) ^ n = -a ^ n
theorem odd.neg_one_pow {α : Type u_2} [monoid α] {n : } (h : odd n) :
(-1) ^ n = -1
theorem odd.pos {α : Type u_2} [nontrivial α] {n : α} (hn : odd n) :
0 < n
@[simp]
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
@[simp]
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 odd_abs {α : Type u_2} [ring α] {a : α} [linear_order α] :
odd a
theorem even.pow_nonneg {R : Type u_4} {n : } (hn : even n) (a : R) :
0 a ^ n
theorem even.pow_pos {R : Type u_4} {a : R} {n : } (hn : even n) (ha : a 0) :
0 < a ^ n
theorem odd.pow_nonpos {R : Type u_4} {a : R} {n : } (hn : odd n) (ha : a 0) :
a ^ n 0
theorem odd.pow_neg {R : Type u_4} {a : R} {n : } (hn : odd n) (ha : a < 0) :
a ^ n < 0
theorem odd.pow_nonneg_iff {R : Type u_4} {a : R} {n : } (hn : odd n) :
0 a ^ n 0 a
theorem odd.pow_nonpos_iff {R : Type u_4} {a : R} {n : } (hn : odd n) :
a ^ n 0 a 0
theorem odd.pow_pos_iff {R : Type u_4} {a : R} {n : } (hn : odd n) :
0 < a ^ n 0 < a
theorem odd.pow_neg_iff {R : Type u_4} {a : R} {n : } (hn : odd n) :
a ^ n < 0 a < 0
theorem even.pow_pos_iff {R : Type u_4} {a : R} {n : } (hn : even n) (h₀ : 0 < n) :
0 < a ^ n a 0
theorem even.pow_abs {R : Type u_4} {p : } (hp : even p) (a : R) :
|a| ^ p = a ^ p
@[simp]
theorem pow_bit0_abs {R : Type u_4} (a : R) (p : ) :
|a| ^ bit0 p = a ^ bit0 p
theorem odd.strict_mono_pow {R : Type u_4} {n : } (hn : odd n) :
strict_mono (λ (a : R), a ^ n)