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

def IsSquare {α : Type u_2} [Mul α] (a : α) : Prop

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

Equations

• IsSquare a = ∃ (r : α), a = r * r

@[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 : α} : Even (AddOpposite.op a) ↔ Even a

abbrev even_op_iff.match_1 {α : Type u_1} [Add α] {a : α} (motive : Even (AddOpposite.op a) → Prop) : ∀ (x : Even (AddOpposite.op a)), (∀ (c : αᵃᵒᵖ) (hc : AddOpposite.op a = c + c), motive ⋯) → motive x

Equations

• ⋯ = ⋯

abbrev even_op_iff.match_2 {α : Type u_1} [Add α] {a : α} (motive : Even a → Prop) : ∀ (x : Even a), (∀ (c : α) (hc : a = c + c), motive ⋯) → motive x

Equations

• ⋯ = ⋯

theorem isSquare_op_iff {α : Type u_2} [Mul α] {a : α} : IsSquare (MulOpposite.op a) ↔ IsSquare a

theorem even_unop_iff {α : Type u_2} [Add α] {a : αᵃᵒᵖ} : Even (AddOpposite.unop a) ↔ Even a

theorem isSquare_unop_iff {α : Type u_2} [Mul α] {a : αᵐᵒᵖ} : IsSquare (MulOpposite.unop a) ↔ IsSquare a

instance instDecidablePredAddOppositeEvenInstAdd {α : Type u_2} [Add α] [DecidablePred Even] : DecidablePred Even

Equations

• instDecidablePredAddOppositeEvenInstAdd x = decidable_of_iff (Even (AddOpposite.unop x)) ⋯

instance instDecidablePredMulOppositeIsSquareInstMul {α : Type u_2} [Mul α] [DecidablePred IsSquare] : DecidablePred IsSquare

Equations

• instDecidablePredMulOppositeIsSquareInstMul x = decidable_of_iff (IsSquare (MulOpposite.unop x)) ⋯

@[simp]

theorem even_ofMul_iff {α : Type u_2} [Mul α] {a : α} : Even (Additive.ofMul a) ↔ IsSquare a

@[simp]

theorem isSquare_toMul_iff {α : Type u_2} [Mul α] {a : Additive α} : IsSquare (Additive.toMul a) ↔ Even a

instance instDecidablePredAdditiveEvenAdd {α : Type u_2} [Mul α] [DecidablePred IsSquare] : DecidablePred Even

Equations

• instDecidablePredAdditiveEvenAdd x = decidable_of_iff (IsSquare (Additive.toMul x)) ⋯

@[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 : Multiplicative α} : Even (Multiplicative.toAdd a) ↔ IsSquare a

instance instDecidablePredMultiplicativeIsSquareMul {α : Type u_2} [Add α] [DecidablePred Even] : DecidablePred IsSquare

Equations

• instDecidablePredMultiplicativeIsSquareMul x = decidable_of_iff (Even (Multiplicative.toAdd x)) ⋯

@[simp]

theorem even_zero {α : Type u_2} [AddZeroClass α] : Even 0

@[simp]

theorem isSquare_one {α : Type u_2} [MulOneClass α] : IsSquare 1

theorem Even.map {F : Type u_1} {α : Type u_2} {β : Type u_3} [AddZeroClass α] [AddZeroClass β] [FunLike F α β] [AddMonoidHomClass F α β] {m : α} (f : F) : Even m → Even (f m)

theorem IsSquare.map {F : Type u_1} {α : Type u_2} {β : Type u_3} [MulOneClass α] [MulOneClass β] [FunLike F α β] [MonoidHomClass F α β] {m : α} (f : F) : IsSquare m → IsSquare (f m)

theorem even_iff_exists_two_nsmul {α : Type u_2} [AddMonoid α] (m : α) : Even m ↔ ∃ (c : α), m = 2 • c

theorem isSquare_iff_exists_sq {α : Type u_2} [Monoid α] (m : α) : IsSquare m ↔ ∃ (c : α), m = c ^ 2

theorem IsSquare.exists_sq {α : Type u_2} [Monoid α] (m : α) : IsSquare m → ∃ (c : α), m = c ^ 2

Alias of the forward direction of isSquare_iff_exists_sq.

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

Alias of the reverse direction of isSquare_iff_exists_sq.

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

Alias of the forwards direction of even_iff_exists_two_nsmul.

theorem Even.nsmul {α : Type u_2} [AddMonoid α] {a : α} (n : ℕ) : Even a → Even (n • a)

theorem IsSquare.pow {α : Type u_2} [Monoid α] {a : α} (n : ℕ) : IsSquare a → IsSquare (a ^ n)

theorem Even.nsmul' {α : Type u_2} [AddMonoid α] {n : ℕ} : Even n → ∀ (a : α), Even (n • a)

theorem Even.isSquare_pow {α : Type u_2} [Monoid α] {n : ℕ} : Even n → ∀ (a : α), IsSquare (a ^ n)

theorem even_two_nsmul {α : Type u_2} [AddMonoid α] (a : α) : Even (2 • a)

theorem IsSquare_sq {α : Type u_2} [Monoid α] (a : α) : IsSquare (a ^ 2)

@[simp]

theorem Even.neg_pow {α : Type u_2} [Monoid α] {n : ℕ} [HasDistribNeg α] : Even n → ∀ (a : α), (-a) ^ n = a ^ n

theorem Even.neg_one_pow {α : Type u_2} [Monoid α] {n : ℕ} [HasDistribNeg α] (h : Even n) : (-1) ^ n = 1

theorem Even.add {α : Type u_2} [AddCommSemigroup α] {a : α} {b : α} : Even a → Even b → Even (a + b)

theorem IsSquare.mul {α : Type u_2} [CommSemigroup α] {a : α} {b : α} : IsSquare a → IsSquare b → IsSquare (a * b)

@[simp]

theorem isSquare_zero (α : Type u_2) [MulZeroClass α] : IsSquare 0

@[simp]

theorem even_neg {α : Type u_2} [SubtractionMonoid α] {a : α} : Even (-a) ↔ Even a

@[simp]

theorem isSquare_inv {α : Type u_2} [DivisionMonoid α] {a : α} : IsSquare a⁻¹ ↔ IsSquare a

theorem IsSquare.inv {α : Type u_2} [DivisionMonoid α] {a : α} : IsSquare a → IsSquare a⁻¹

Alias of the reverse direction of isSquare_inv.

theorem Even.neg {α : Type u_2} [SubtractionMonoid α] {a : α} : Even a → Even (-a)

theorem Even.zsmul {α : Type u_2} [SubtractionMonoid α] {a : α} (n : ℤ) : Even a → Even (n • a)

theorem IsSquare.zpow {α : Type u_2} [DivisionMonoid α] {a : α} (n : ℤ) : IsSquare a → IsSquare (a ^ n)

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

theorem even_abs {α : Type u_2} [AddGroup α] [LinearOrder α] {a : α} : Even |a| ↔ Even a

theorem Even.sub {α : Type u_2} [SubtractionCommMonoid α] {a : α} {b : α} (ha : Even a) (hb : Even b) : Even (a - b)

theorem IsSquare.div {α : Type u_2} [DivisionCommMonoid α] {a : α} {b : α} (ha : IsSquare a) (hb : IsSquare b) : IsSquare (a / b)

@[simp]

theorem Even.zsmul' {α : Type u_2} [AddGroup α] {n : ℤ} : Even n → ∀ (a : α), Even (n • a)

@[simp]

theorem Even.isSquare_zpow {α : Type u_2} [Group α] {n : ℤ} : Even n → ∀ (a : α), IsSquare (a ^ n)

theorem Even.tsub {α : Type u_2} [CanonicallyLinearOrderedAddCommMonoid α] [Sub α] [OrderedSub α] [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} [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 : α} : Even a → 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))

@[simp]

theorem one_add_self_self {α : Type u_2} [Semiring α] {a : α} : Odd (1 + a + 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)

@[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 Odd.pos {α : Type u_2} [CanonicallyOrderedCommSemiring α] [Nontrivial α] {a : α} (hn : Odd a) : 0 < a

theorem even_neg_two {α : Type u_2} [Ring α] : Even (-2)

theorem Odd.neg {α : Type u_2} [Ring α] {a : α} (ha : 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 : α} [LinearOrder α] : Odd |a| ↔ Odd a

Lemmas for canonically linear ordered semirings or linear ordered rings

The slightly unusual typeclass assumptions [LinearOrderedSemiring R] [ExistsAddOfLE R] cover two more familiar settings:

• [LinearOrderedRing R], eg ℤ, ℚ or ℝ
• [CanonicallyLinearOrderedSemiring R] (although we don't actually have this typeclass), eg ℕ, ℚ≥0 or ℝ≥0

theorem Even.pow_nonneg {R : Type u_4} [LinearOrderedSemiring R] [ExistsAddOfLE R] {n : ℕ} (hn : Even n) (a : R) : 0 ≤ a ^ n

theorem Even.pow_pos {R : Type u_4} [LinearOrderedSemiring R] [ExistsAddOfLE R] {a : R} {n : ℕ} (hn : Even n) (ha : a ≠ 0) : 0 < a ^ n

theorem Odd.pow_neg_iff {R : Type u_4} [LinearOrderedSemiring R] [ExistsAddOfLE R] {a : R} {n : ℕ} (hn : Odd n) : a ^ n < 0 ↔ a < 0

theorem Odd.pow_nonneg_iff {R : Type u_4} [LinearOrderedSemiring R] [ExistsAddOfLE R] {a : R} {n : ℕ} (hn : Odd n) : 0 ≤ a ^ n ↔ 0 ≤ a

theorem Odd.pow_nonpos_iff {R : Type u_4} [LinearOrderedSemiring R] [ExistsAddOfLE R] {a : R} {n : ℕ} (hn : Odd n) : a ^ n ≤ 0 ↔ a ≤ 0

theorem Odd.pow_pos_iff {R : Type u_4} [LinearOrderedSemiring R] [ExistsAddOfLE R] {a : R} {n : ℕ} (hn : Odd n) : 0 < a ^ n ↔ 0 < a

theorem Odd.pow_nonpos {R : Type u_4} [LinearOrderedSemiring R] [ExistsAddOfLE R] {a : R} {n : ℕ} (hn : Odd n) : a ≤ 0 → a ^ n ≤ 0

Alias of the reverse direction of Odd.pow_nonpos_iff.

theorem Odd.pow_neg {R : Type u_4} [LinearOrderedSemiring R] [ExistsAddOfLE R] {a : R} {n : ℕ} (hn : Odd n) : a < 0 → a ^ n < 0

Alias of the reverse direction of Odd.pow_neg_iff.

theorem Even.pow_pos_iff {R : Type u_4} [LinearOrderedSemiring R] [ExistsAddOfLE R] {a : R} {n : ℕ} (hn : Even n) (h₀ : n ≠ 0) : 0 < a ^ n ↔ a ≠ 0

theorem Odd.strictMono_pow {R : Type u_4} [LinearOrderedSemiring R] [ExistsAddOfLE R] {n : ℕ} (hn : Odd n) : StrictMono fun (a : R) => a ^ n

theorem Even.pow_abs {R : Type u_4} [LinearOrderedRing R] {p : ℕ} (hp : Even p) (a : R) : |a| ^ p = a ^ p

@[simp]

theorem pow_bit0_abs {R : Type u_4} [LinearOrderedRing R] (a : R) (p : ℕ) : |a| ^ bit0 p = a ^ bit0 p