# Squares, even and odd elements #

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

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

IsSquare 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 IsSquare/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 Even {α : Type u_2} [Add α] (a : α) :

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

Equations
Instances For
def IsSquare {α : Type u_2} [Mul α] (a : α) :

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

Equations
• = ∃ (r : α), a = r * r
Instances For
@[simp]
theorem even_add_self {α : Type u_2} [Add α] (m : α) :
Even (m + m)
@[simp]
theorem isSquare_mul_self {α : Type u_2} [Mul α] (m : α) :
IsSquare (m * m)
theorem even_op_iff {α : Type u_2} [Add α] {a : α} :
abbrev even_op_iff.match_1 {α : Type u_1} [Add α] {a : α} (motive : Prop) :
∀ (x : ), (∀ (c : αᵃᵒᵖ) (hc : = c + c), motive )motive x
Equations
• =
Instances For
abbrev even_op_iff.match_2 {α : Type u_1} [Add α] {a : α} (motive : Even aProp) :
∀ (x : Even a), (∀ (c : α) (hc : a = c + c), motive )motive x
Equations
• =
Instances For
theorem isSquare_op_iff {α : Type u_2} [Mul α] {a : α} :
theorem even_unop_iff {α : Type u_2} [Add α] {a : αᵃᵒᵖ} :
theorem isSquare_unop_iff {α : Type u_2} [Mul α] {a : αᵐᵒᵖ} :
Equations
@[simp]
theorem even_ofMul_iff {α : Type u_2} [Mul α] {a : α} :
@[simp]
theorem isSquare_toMul_iff {α : Type u_2} [Mul α] {a : } :
IsSquare (Additive.toMul a) Even a
instance instDecidablePredAdditiveEvenAdd {α : Type u_2} [Mul α] [DecidablePred IsSquare] :
Equations
@[simp]
theorem isSquare_ofAdd_iff {α : Type u_2} [Add α] {a : α} :
IsSquare (Multiplicative.ofAdd a) Even a
@[simp]
theorem even_toAdd_iff {α : Type u_2} [Add α] {a : } :
Equations
@[simp]
theorem even_zero {α : Type u_2} [] :
@[simp]
theorem isSquare_one {α : Type u_2} [] :
theorem Even.map {F : Type u_1} {α : Type u_2} {β : Type u_3} [] [] [FunLike F α β] [] {m : α} (f : F) :
Even mEven (f m)
theorem IsSquare.map {F : Type u_1} {α : Type u_2} {β : Type u_3} [] [] [FunLike F α β] [] {m : α} (f : F) :
IsSquare (f m)
theorem even_iff_exists_two_nsmul {α : Type u_2} [] (m : α) :
Even m ∃ (c : α), m = 2 c
theorem isSquare_iff_exists_sq {α : Type u_2} [] (m : α) :
∃ (c : α), m = c ^ 2
theorem IsSquare.exists_sq {α : Type u_2} [] (m : α) :
∃ (c : α), m = c ^ 2

Alias of the forward direction of isSquare_iff_exists_sq.

theorem isSquare_of_exists_sq {α : Type u_2} [] (m : α) :
(∃ (c : α), m = c ^ 2)

Alias of the reverse direction of isSquare_iff_exists_sq.

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

Alias of the forwards direction of even_iff_exists_two_nsmul.

theorem Even.nsmul {α : Type u_2} [] {a : α} (n : ) :
Even aEven (n a)
theorem IsSquare.pow {α : Type u_2} [] {a : α} (n : ) :
IsSquare (a ^ n)
theorem Even.nsmul' {α : Type u_2} [] {n : } :
Even n∀ (a : α), Even (n a)
theorem Even.isSquare_pow {α : Type u_2} [] {n : } :
Even n∀ (a : α), IsSquare (a ^ n)
theorem even_two_nsmul {α : Type u_2} [] (a : α) :
Even (2 a)
theorem IsSquare_sq {α : Type u_2} [] (a : α) :
IsSquare (a ^ 2)
@[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.add {α : Type u_2} [] {a : α} {b : α} :
Even aEven bEven (a + b)
theorem IsSquare.mul {α : Type u_2} [] {a : α} {b : α} :
IsSquare (a * b)
@[simp]
theorem isSquare_zero (α : Type u_2) [] :
@[simp]
theorem even_neg {α : Type u_2} {a : α} :
Even (-a) Even a
@[simp]
theorem isSquare_inv {α : Type u_2} [] {a : α} :
theorem IsSquare.inv {α : Type u_2} [] {a : α} :

Alias of the reverse direction of isSquare_inv.

theorem Even.neg {α : Type u_2} {a : α} :
Even aEven (-a)
theorem Even.zsmul {α : Type u_2} {a : α} (n : ) :
Even aEven (n a)
theorem IsSquare.zpow {α : Type u_2} [] {a : α} (n : ) :
IsSquare (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} [] [] {a : α} :
Even |a| Even a
theorem Even.sub {α : Type u_2} {a : α} {b : α} (ha : Even a) (hb : Even b) :
Even (a - b)
theorem IsSquare.div {α : Type u_2} {a : α} {b : α} (ha : ) (hb : ) :
IsSquare (a / b)
@[simp]
theorem Even.zsmul' {α : Type u_2} [] {n : } :
Even n∀ (a : α), Even (n a)
@[simp]
theorem Even.isSquare_zpow {α : Type u_2} [] {n : } :
Even n∀ (a : α), IsSquare (a ^ n)
theorem Even.tsub {α : Type u_2} [Sub α] [] [ContravariantClass α α (fun (x x_1 : α) => x + x_1) fun (x x_1 : α) => x x_1] {m : α} {n : α} (hm : Even m) (hn : Even n) :
Even (m - n)
theorem even_iff_exists_bit0 {α : Type u_2} [Add α] {a : α} :
Even a ∃ (b : α), a = bit0 b
theorem Even.exists_bit0 {α : Type u_2} [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} [] (m : α) :
Even m ∃ (c : α), m = 2 * c
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} [] {m : α} {n : α} (hm : Even m) (hn : m n) :
theorem Dvd.dvd.even {α : Type u_2} [] {m : α} {n : α} (hn : m n) (hm : Even m) :
@[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} [] {m : α} (hm : Even m) (n : α) :
Even (n * m)
@[simp]
theorem Even.mul_right {α : Type u_2} [] {m : α} (hm : Even m) (n : α) :
Even (m * n)
theorem even_two_mul {α : Type u_2} [] (m : α) :
Even (2 * m)
theorem Even.pow_of_ne_zero {α : Type u_2} [] {m : α} (hm : Even m) {a : } :
a 0Even (m ^ a)
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} [] {m : α} {n : α} :
Even mOdd nOdd (m + n)
theorem Even.odd_add {α : Type u_2} [] {m : α} {n : α} :
Even mOdd nOdd (n + m)
theorem Odd.add_even {α : Type u_2} [] {m : α} {n : α} (hm : Odd m) (hn : Even n) :
Odd (m + n)
theorem Odd.add_odd {α : Type u_2} [] {m : α} {n : α} :
Odd mOdd nEven (m + n)
@[simp]
theorem odd_one {α : Type u_2} [] :
Odd 1
@[simp]
theorem Even.add_one {α : Type u_2} [] {m : α} (h : Even m) :
Odd (m + 1)
@[simp]
theorem Even.one_add {α : Type u_2} [] {m : α} (h : Even m) :
Odd (1 + m)
theorem odd_two_mul_add_one {α : Type u_2} [] (m : α) :
Odd (2 * m + 1)
@[simp]
theorem odd_add_self_one' {α : Type u_2} [] {m : α} :
Odd (m + (m + 1))
@[simp]
theorem odd_add_one_self {α : Type u_2} [] {m : α} :
Odd (m + 1 + m)
@[simp]
theorem odd_add_one_self' {α : Type u_2} [] {m : α} :
Odd (m + (1 + m))
@[simp]
theorem one_add_self_self {α : Type u_2} [] {m : α} :
Odd (1 + m + m)
theorem Odd.map {F : Type u_1} {α : Type u_2} {β : Type u_3} [] [] {m : α} [FunLike F α β] [RingHomClass F α β] (f : F) :
Odd mOdd (f m)
@[simp]
theorem Odd.mul {α : Type u_2} [] {m : α} {n : α} :
Odd mOdd nOdd (m * n)
theorem Odd.pow {α : Type u_2} [] {m : α} (hm : Odd m) {a : } :
Odd (m ^ a)
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 Odd.pos {α : Type u_2} [] {n : α} (hn : Odd n) :
0 < n
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 odd_abs {α : Type u_2} [Ring α] {a : α} [] :
Odd |a| 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₀ : n 0) :
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.strictMono_pow {R : Type u_4} {n : } (hn : Odd n) :
StrictMono fun (a : R) => a ^ n