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
↔ ∃ r, a = r * r
Even a ↔ ∃ r, a = r + r
∃ r, a = r * r
Even a ↔ ∃ r, a = r + r
↔ ∃ r, a = r + r
∃ 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← two_mul. It might be the case that by making a careful choice of simp lemma, this can be avoided.

ink

def Even {α : Type u_1} [inst : 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

ink

def IsSquare {α : Type u_1} [inst : 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

ink

@[simp]

theorem even_add_self {α : Type u_1} [inst : Add α] (m : α) : Even (m + m)

ink

@[simp]

theorem isSquare_mul_self {α : Type u_1} [inst : Mul α] (m : α) : IsSquare (m * m)

ink

abbrev even_op_iff.match_1 {α : Type u_1} [inst : Add α] (a : α) (motive : Even { unop := a } → Prop) : (x : Even { unop := a }) → ((c : αᵃᵒᵖ) → (hc : { unop := a } = c + c) → motive (_ : ∃ r, { unop := a } = r + r)) → motive x

Equations

• even_op_iff.match_1 a motive x h_1 = Exists.casesOn x fun w h => h_1 w h

ink

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

Equations

• even_op_iff.match_2 a motive x h_1 = Exists.casesOn x fun w h => h_1 w h

ink

theorem even_op_iff {α : Type u_1} [inst : Add α] (a : α) : Even { unop := a } ↔ Even a

ink

theorem isSquare_op_iff {α : Type u_1} [inst : Mul α] (a : α) : IsSquare { unop := a } ↔ IsSquare a

ink

@[simp]

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

ink

@[simp]

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

ink

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

ink

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

ink

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

ink

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

ink

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

Alias of the forward direction of isSquare_iff_exists_sq.

ink

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

Alias of the reverse direction of isSquare_iff_exists_sq.

ink

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

Alias of the forwards direction of even_iff_exists_two_nsmul.

ink

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

ink

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

ink

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

ink

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

ink

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

ink

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

ink

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

ink

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

ink

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

ink

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

ink

@[simp]

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

ink

@[simp]

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

ink

@[simp]

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

ink

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

Alias of the reverse direction of isSquare_inv.

ink

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

ink

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

ink

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

ink

theorem Even.neg_zpow {α : Type u_1} [inst : DivisionMonoid α] [inst : HasDistribNeg α] {n : ℤ} : Even n → ∀ (a : α), (-a) ^ n = a ^ n

ink

theorem Even.neg_one_zpow {α : Type u_1} [inst : DivisionMonoid α] [inst : HasDistribNeg α] {n : ℤ} (h : Even n) : (-1) ^ n = 1

ink

theorem even_abs {α : Type u_1} [inst : SubtractionMonoid α] [inst : LinearOrder α] {a : α} : Even (abs a) ↔ Even a

ink

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

ink

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

ink

@[simp]

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

ink

@[simp]

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

ink

theorem Even.tsub {α : Type u_1} [inst : CanonicallyLinearOrderedAddMonoid α] [inst : Sub α] [inst : OrderedSub α] [inst : 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)

ink

theorem even_iff_exists_bit0 {α : Type u_1} [inst : Add α] {a : α} : Even a ↔ ∃ b, a = bit0 b

ink

theorem Even.exists_bit0 {α : Type u_1} [inst : Add α] {a : α} : Even a → ∃ b, a = bit0 b

Alias of the forward direction of even_iff_exists_bit0.

ink

theorem even_iff_exists_two_mul {α : Type u_1} [inst : Semiring α] (m : α) : Even m ↔ ∃ c, m = 2 * c

ink

theorem even_iff_two_dvd {α : Type u_1} [inst : Semiring α] {a : α} : Even a ↔ 2 ∣ a

ink

theorem Even.two_dvd {α : Type u_1} [inst : Semiring α] {a : α} : Even a → 2 ∣ a

Alias of the forward direction of even_iff_two_dvd.

ink

theorem Even.trans_dvd {α : Type u_1} [inst : Semiring α] {m : α} {n : α} (hm : Even m) (hn : m ∣ n) : Even n

ink

theorem Dvd.dvd.even {α : Type u_1} [inst : Semiring α] {m : α} {n : α} (hn : m ∣ n) (hm : Even m) : Even n

ink

@[simp]

theorem range_two_mul (α : Type u_1) [inst : Semiring α] : (Set.range fun x => 2 * x) = { a | Even a }

ink

@[simp]

theorem even_bit0 {α : Type u_1} [inst : Semiring α] (a : α) : Even (bit0 a)

ink

@[simp]

theorem even_two {α : Type u_1} [inst : Semiring α] : Even 2

ink

@[simp]

theorem Even.mul_left {α : Type u_1} [inst : Semiring α] {m : α} (hm : Even m) (n : α) : Even (n * m)

ink

@[simp]

theorem Even.mul_right {α : Type u_1} [inst : Semiring α] {m : α} (hm : Even m) (n : α) : Even (m * n)

ink

theorem even_two_mul {α : Type u_1} [inst : Semiring α] (m : α) : Even (2 * m)

ink

theorem Even.pow_of_ne_zero {α : Type u_1} [inst : Semiring α] {m : α} (hm : Even m) {a : ℕ} : a ≠ 0 → Even (m ^ a)

ink

def Odd {α : Type u_1} [inst : 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

ink

theorem odd_iff_exists_bit1 {α : Type u_1} [inst : Semiring α] {a : α} : Odd a ↔ ∃ b, a = bit1 b

ink

theorem Odd.exists_bit1 {α : Type u_1} [inst : Semiring α] {a : α} : Odd a → ∃ b, a = bit1 b

Alias of the forward direction of odd_iff_exists_bit1.

ink

@[simp]

theorem odd_bit1 {α : Type u_1} [inst : Semiring α] (a : α) : Odd (bit1 a)

ink

@[simp]

theorem range_two_mul_add_one (α : Type u_1) [inst : Semiring α] : (Set.range fun x => 2 * x + 1) = { a | Odd a }

ink

theorem Even.add_odd {α : Type u_1} [inst : Semiring α] {m : α} {n : α} : Even m → Odd n → Odd (m + n)

ink

theorem Odd.add_even {α : Type u_1} [inst : Semiring α] {m : α} {n : α} (hm : Odd m) (hn : Even n) : Odd (m + n)

ink

theorem Odd.add_odd {α : Type u_1} [inst : Semiring α] {m : α} {n : α} : Odd m → Odd n → Even (m + n)

ink

@[simp]

theorem odd_one {α : Type u_1} [inst : Semiring α] : Odd 1

ink

@[simp]

theorem odd_two_mul_add_one {α : Type u_1} [inst : Semiring α] (m : α) : Odd (2 * m + 1)

ink

theorem Odd.map {F : Type u_1} {α : Type u_2} {β : Type u_3} [inst : Semiring α] [inst : Semiring β] {m : α} [inst : RingHomClass F α β] (f : F) : Odd m → Odd (↑f m)

ink

@[simp]

theorem Odd.mul {α : Type u_1} [inst : Semiring α] {m : α} {n : α} : Odd m → Odd n → Odd (m * n)

ink

theorem Odd.pow {α : Type u_1} [inst : Semiring α] {m : α} (hm : Odd m) {a : ℕ} : Odd (m ^ a)

ink

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

ink

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

ink

theorem Odd.pos {α : Type u_1} [inst : CanonicallyOrderedCommSemiring α] [inst : Nontrivial α] {n : α} (hn : Odd n) : 0 < n

ink

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

ink

theorem Odd.neg {α : Type u_1} [inst : Ring α] {a : α} (hp : Odd a) : Odd (-a)

ink

@[simp]

theorem odd_neg {α : Type u_1} [inst : Ring α] {a : α} : Odd (-a) ↔ Odd a

ink

theorem odd_neg_one {α : Type u_1} [inst : Ring α] : Odd (-1)

ink

theorem Odd.sub_even {α : Type u_1} [inst : Ring α] {a : α} {b : α} (ha : Odd a) (hb : Even b) : Odd (a - b)

ink

theorem Even.sub_odd {α : Type u_1} [inst : Ring α] {a : α} {b : α} (ha : Even a) (hb : Odd b) : Odd (a - b)

ink

theorem Odd.sub_odd {α : Type u_1} [inst : Ring α] {a : α} {b : α} (ha : Odd a) (hb : Odd b) : Even (a - b)

ink

theorem odd_abs {α : Type u_1} [inst : Ring α] {a : α} [inst : LinearOrder α] : Odd (abs a) ↔ Odd a

ink

theorem Even.pow_nonneg {R : Type u_1} [inst : LinearOrderedRing R] {n : ℕ} (hn : Even n) (a : R) : 0 ≤ a ^ n

ink

theorem Even.pow_pos {R : Type u_1} [inst : LinearOrderedRing R] {a : R} {n : ℕ} (hn : Even n) (ha : a ≠ 0) : 0 < a ^ n

ink

theorem Odd.pow_nonpos {R : Type u_1} [inst : LinearOrderedRing R] {a : R} {n : ℕ} (hn : Odd n) (ha : a ≤ 0) : a ^ n ≤ 0

ink

theorem Odd.pow_neg {R : Type u_1} [inst : LinearOrderedRing R] {a : R} {n : ℕ} (hn : Odd n) (ha : a < 0) : a ^ n < 0

ink

theorem Odd.pow_nonneg_iff {R : Type u_1} [inst : LinearOrderedRing R] {a : R} {n : ℕ} (hn : Odd n) : 0 ≤ a ^ n ↔ 0 ≤ a

ink

theorem Odd.pow_nonpos_iff {R : Type u_1} [inst : LinearOrderedRing R] {a : R} {n : ℕ} (hn : Odd n) : a ^ n ≤ 0 ↔ a ≤ 0

ink

theorem Odd.pow_pos_iff {R : Type u_1} [inst : LinearOrderedRing R] {a : R} {n : ℕ} (hn : Odd n) : 0 < a ^ n ↔ 0 < a

ink

theorem Odd.pow_neg_iff {R : Type u_1} [inst : LinearOrderedRing R] {a : R} {n : ℕ} (hn : Odd n) : a ^ n < 0 ↔ a < 0

ink

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

ink

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

ink

@[simp]

theorem pow_bit0_abs {R : Type u_1} [inst : LinearOrderedRing R] (a : R) (p : ℕ) : abs a ^ bit0 p = a ^ bit0 p

ink

theorem Odd.strictMono_pow {R : Type u_1} [inst : LinearOrderedRing R] {n : ℕ} (hn : Odd n) : StrictMono fun a => a ^ n

ink

def Parser.Attr.parity_simps : Lean.ParserDescr

Simp attribute for lemmas about even

Equations

• One or more equations did not get rendered due to their size.