algebra.parity

# Squares, even and odd elements #

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 square a if a = r * r, for some r : α.

Equations
• = ∃ (r : α), a = r * r
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 : α) :
@[protected, instance]
def is_square_decidable {α : Type u_2} [has_mul α] [fintype α] [decidable_eq α] :

Create a decidability instance for is_square on fintypes.

Equations
@[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) :
is_square (f m)
theorem even.map {F : Type u_1} {α : Type u_2} {β : Type u_3} [ β] {m : α} (f : F) :
even meven (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.

@[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_zero (M : Type u_1)  :

0 is always a square (in a monoid with zero).

theorem is_square.mul {α : Type u_2} {a b : α} :
is_square (a * b)
theorem even.add {α : Type u_2} {a b : α} :
even aeven beven (a + b)
@[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 aeven (-a)

Alias of the reverse direction of is_square_inv.

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)
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
@[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 0even (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
• odd a = ∃ (k : α), a = 2 * k + 1
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 modd nodd (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 modd neven (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 modd (f m)
@[simp]
theorem odd.mul {α : Type u_2} [semiring α] {m n : α} :
odd modd nodd (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)
theorem fintype.card_fin_even {k : } :

The cardinality of fin (bit0 k) is even, fact version. This fact is needed as an instance by matrix.special_linear_group.has_neg.

theorem odd.neg_zpow {K : Type u_5} {n : } (h : odd n) (a : K) :
(-a) ^ n = -a ^ n
theorem odd.neg_one_zpow {K : Type u_5} {n : } (h : odd n) :
(-1) ^ n = -1
@[protected]
theorem even.zpow_nonneg {K : Type u_5} {n : } (hn : even n) (a : K) :
0 a ^ n
theorem even.zpow_pos {K : Type u_5} {n : } {a : K} (hn : even n) (ha : a 0) :
0 < a ^ n
@[protected]
theorem odd.zpow_nonneg {K : Type u_5} {n : } {a : K} (hn : odd n) (ha : 0 a) :
0 a ^ n
theorem odd.zpow_pos {K : Type u_5} {n : } {a : K} (hn : odd n) (ha : 0 < a) :
0 < a ^ n
theorem odd.zpow_nonpos {K : Type u_5} {n : } {a : K} (hn : odd n) (ha : a 0) :
a ^ n 0
theorem odd.zpow_neg {K : Type u_5} {n : } {a : K} (hn : odd n) (ha : a < 0) :
a ^ n < 0
theorem even.zpow_abs {K : Type u_5} {p : } (hp : even p) (a : K) :
|a| ^ p = a ^ p
@[simp]
theorem zpow_bit0_abs {K : Type u_5} (a : K) (p : ) :
|a| ^ bit0 p = a ^ bit0 p
theorem even.abs_zpow {K : Type u_5} {p : } (hp : even p) (a : K) :
|a ^ p| = a ^ p
@[simp]
theorem abs_zpow_bit0 {K : Type u_5} (a : K) (p : ) :
|a ^ bit0 p| = a ^ bit0 p