mathlib documentation

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

is_square a = ∃ (r : α), a = r * r

Instances for is_square

is_square_decidable

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

even a = ∃ (r : α), a = r + r

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 : α) :

even (add_opposite.op a) ↔ even a

theorem is_square_op_iff {α : Type u_2} [has_mul α] (a : α) :

is_square (mul_opposite.op a) ↔ is_square a

@[protected, instance]

def is_square_decidable {α : Type u_2} [has_mul α] [fintype α] [decidable_eq α] :

decidable_pred is_square

Create a decidability instance for is_square on fintypes.

Equations

is_square_decidable = λ (a : α), fintype.decidable_exists_fintype

@[simp]

theorem even_zero {α : Type u_2} [add_zero_class α] :

@[simp]

theorem is_square_one {α : Type u_2} [mul_one_class α] :

theorem is_square.map {F : Type u_1} {α : Type u_2} {β : Type u_3} [mul_one_class α] [mul_one_class β] [monoid_hom_class F α β] {m : α} (f : F) :

is_square m → is_square (⇑f m)

theorem even.map {F : Type u_1} {α : Type u_2} {β : Type u_3} [add_zero_class α] [add_zero_class β] [add_monoid_hom_class F α β] {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 : α) :

is_square m ↔ ∃ (c : α), m = c ^ 2

theorem is_square_of_exists_sq {α : Type u_2} [monoid α] (m : α) :

(∃ (c : α), m = c ^ 2) → is_square m

Alias of the reverse direction of is_square_iff_exists_sq.

theorem is_square.exists_sq {α : Type u_2} [monoid α] (m : α) :

is_square 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 α] [has_distrib_neg α] {n : ℕ} :

even n → ∀ (a : α), (-a) ^ n = a ^ n

theorem even.neg_one_pow {α : Type u_2} [monoid α] [has_distrib_neg α] {n : ℕ} (h : even n) :

(-1) ^ n = 1

theorem is_square_zero (M : Type u_1) [monoid_with_zero M] :

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

theorem is_square.mul {α : Type u_2} [comm_semigroup α] {a b : α} :

is_square a → is_square b → is_square (a * b)

theorem even.add {α : Type u_2} [add_comm_semigroup α] {a b : α} :

even a → even b → even (a + b)

@[simp]

theorem even_neg {α : Type u_2} [subtraction_monoid α] {a : α} :

even (-a) ↔ even a

@[simp]

theorem is_square_inv {α : Type u_2} [division_monoid α] {a : α} :

is_square a⁻¹ ↔ is_square a

theorem is_square.inv {α : Type u_2} [division_monoid α] {a : α} :

is_square a → is_square a⁻¹

Alias of the reverse direction of is_square_inv.

theorem even.neg {α : Type u_2} [subtraction_monoid α] {a : α} :

even a → even (-a)

Alias of the reverse direction of is_square_inv.

theorem even.neg_zpow {α : Type u_2} [division_monoid α] [has_distrib_neg α] {n : ℤ} :

even n → ∀ (a : α), (-a) ^ n = a ^ n

theorem even.neg_one_zpow {α : Type u_2} [division_monoid α] [has_distrib_neg α] {n : ℤ} (h : even n) :

(-1) ^ n = 1

theorem even_abs {α : Type u_2} [subtraction_monoid α] [linear_order α] {a : α} :

even |a| ↔ even a

theorem is_square.div {α : Type u_2} [division_comm_monoid α] {a b : α} (ha : is_square a) (hb : is_square b) :

is_square (a / b)

theorem even.sub {α : Type u_2} [subtraction_comm_monoid α] {a b : α} (ha : even a) (hb : even b) :

even (a - b)

theorem even.tsub {α : Type u_2} [canonically_linear_ordered_add_monoid α] [has_sub α] [has_ordered_sub α] [contravariant_class α α has_add.add has_le.le] {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 ≠ 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

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 : α) :

@[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 α] :

@[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 : α} [ring_hom_class F α β] (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 α] [has_distrib_neg α] {n : ℕ} :

odd n → ∀ (a : α), (-a) ^ n = -a ^ n

theorem odd.neg_one_pow {α : Type u_2} [monoid α] [has_distrib_neg α] {n : ℕ} (h : odd n) :

(-1) ^ n = -1

theorem odd.pos {α : Type u_2} [canonically_ordered_comm_semiring α] [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| ↔ odd a

theorem even.pow_nonneg {R : Type u_4} [linear_ordered_ring R] {n : ℕ} (hn : even n) (a : R) :

0 ≤ a ^ n

theorem even.pow_pos {R : Type u_4} [linear_ordered_ring R] {a : R} {n : ℕ} (hn : even n) (ha : a ≠ 0) :

0 < a ^ n

theorem odd.pow_nonpos {R : Type u_4} [linear_ordered_ring R] {a : R} {n : ℕ} (hn : odd n) (ha : a ≤ 0) :

a ^ n ≤ 0

theorem odd.pow_neg {R : Type u_4} [linear_ordered_ring R] {a : R} {n : ℕ} (hn : odd n) (ha : a < 0) :

a ^ n < 0

theorem odd.pow_nonneg_iff {R : Type u_4} [linear_ordered_ring R] {a : R} {n : ℕ} (hn : odd n) :

0 ≤ a ^ n ↔ 0 ≤ a

theorem odd.pow_nonpos_iff {R : Type u_4} [linear_ordered_ring R] {a : R} {n : ℕ} (hn : odd n) :

a ^ n ≤ 0 ↔ a ≤ 0

theorem odd.pow_pos_iff {R : Type u_4} [linear_ordered_ring R] {a : R} {n : ℕ} (hn : odd n) :

0 < a ^ n ↔ 0 < a

theorem odd.pow_neg_iff {R : Type u_4} [linear_ordered_ring R] {a : R} {n : ℕ} (hn : odd n) :

a ^ n < 0 ↔ a < 0

theorem even.pow_pos_iff {R : Type u_4} [linear_ordered_ring R] {a : R} {n : ℕ} (hn : even n) (h₀ : 0 < n) :

0 < a ^ n ↔ a ≠ 0

theorem even.pow_abs {R : Type u_4} [linear_ordered_ring R] {p : ℕ} (hp : even p) (a : R) :

|a| ^ p = a ^ p

@[simp]

theorem pow_bit0_abs {R : Type u_4} [linear_ordered_ring R] (a : R) (p : ℕ) :

|a| ^ bit0 p = a ^ bit0 p

theorem odd.strict_mono_pow {R : Type u_4} [linear_ordered_ring R] {n : ℕ} (hn : odd n) :

strict_mono (λ (a : R), a ^ n)

theorem fintype.card_fin_even {k : ℕ} :

fact (even (fintype.card (fin (bit0 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} [division_ring K] {n : ℤ} (h : odd n) (a : K) :

(-a) ^ n = -a ^ n

theorem odd.neg_one_zpow {K : Type u_5} [division_ring K] {n : ℤ} (h : odd n) :

(-1) ^ n = -1

@[protected]

theorem even.zpow_nonneg {K : Type u_5} [linear_ordered_field K] {n : ℤ} (hn : even n) (a : K) :

0 ≤ a ^ n

theorem even.zpow_pos {K : Type u_5} [linear_ordered_field K] {n : ℤ} {a : K} (hn : even n) (ha : a ≠ 0) :

0 < a ^ n

@[protected]

theorem odd.zpow_nonneg {K : Type u_5} [linear_ordered_field K] {n : ℤ} {a : K} (hn : odd n) (ha : 0 ≤ a) :

0 ≤ a ^ n

theorem odd.zpow_pos {K : Type u_5} [linear_ordered_field K] {n : ℤ} {a : K} (hn : odd n) (ha : 0 < a) :

0 < a ^ n

theorem odd.zpow_nonpos {K : Type u_5} [linear_ordered_field K] {n : ℤ} {a : K} (hn : odd n) (ha : a ≤ 0) :

a ^ n ≤ 0

theorem odd.zpow_neg {K : Type u_5} [linear_ordered_field K] {n : ℤ} {a : K} (hn : odd n) (ha : a < 0) :

a ^ n < 0

theorem even.zpow_abs {K : Type u_5} [linear_ordered_field K] {p : ℤ} (hp : even p) (a : K) :

|a| ^ p = a ^ p

@[simp]

theorem zpow_bit0_abs {K : Type u_5} [linear_ordered_field K] (a : K) (p : ℤ) :

|a| ^ bit0 p = a ^ bit0 p

theorem even.abs_zpow {K : Type u_5} [linear_ordered_field K] {p : ℤ} (hp : even p) (a : K) :

|a ^ p| = a ^ p

@[simp]

theorem abs_zpow_bit0 {K : Type u_5} [linear_ordered_field K] (a : K) (p : ℤ) :

|a ^ bit0 p| = a ^ bit0 p