Documentation

Mathlib.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 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 #

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
    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)
      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 even_op_iff {α : Type u_2} [Add α] {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
        • =
        Instances For
          theorem isSquare_op_iff {α : Type u_2} [Mul α] {a : α} :
          theorem even_unop_iff {α : Type u_2} [Add α] {a : αᵃᵒᵖ} :
          @[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
          @[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
          @[simp]
          theorem even_zero {α : Type u_2} [AddZeroClass α] :
          @[simp]
          theorem isSquare_one {α : Type u_2} [MulOneClass α] :
          theorem Even.map {F : Type u_1} {α : Type u_2} {β : Type u_3} [AddZeroClass α] [AddZeroClass β] [FunLike F α β] [AddMonoidHomClass F α β] {m : α} (f : F) :
          Even mEven (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 mIsSquare (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 aEven (n a)
          theorem IsSquare.pow {α : Type u_2} [Monoid α] {a : α} (n : ) :
          IsSquare aIsSquare (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 aEven bEven (a + b)
          theorem IsSquare.mul {α : Type u_2} [CommSemigroup α] {a : α} {b : α} :
          IsSquare aIsSquare bIsSquare (a * b)
          @[simp]
          theorem isSquare_zero (α : Type u_2) [MulZeroClass α] :
          @[simp]
          theorem even_neg {α : Type u_2} [SubtractionMonoid α] {a : α} :
          Even (-a) Even a
          @[simp]
          theorem isSquare_inv {α : Type u_2} [DivisionMonoid α] {a : α} :
          theorem IsSquare.inv {α : Type u_2} [DivisionMonoid α] {a : α} :

          Alias of the reverse direction of isSquare_inv.

          theorem Even.neg {α : Type u_2} [SubtractionMonoid α] {a : α} :
          Even aEven (-a)
          theorem Even.zsmul {α : Type u_2} [SubtractionMonoid α] {a : α} (n : ) :
          Even aEven (n a)
          theorem IsSquare.zpow {α : Type u_2} [DivisionMonoid α] {a : α} (n : ) :
          IsSquare aIsSquare (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 α] (m : α) :
          Even m ∃ (c : α), m = 2 * c
          theorem even_iff_two_dvd {α : Type u_2} [Semiring α] {a : α} :
          Even a 2 a
          theorem Even.two_dvd {α : Type u_2} [Semiring α] {a : α} :
          Even a2 a

          Alias of the forward direction of even_iff_two_dvd.

          theorem Even.trans_dvd {α : Type u_2} [Semiring α] {m : α} {n : α} (hm : Even m) (hn : m n) :
          theorem Dvd.dvd.even {α : Type u_2} [Semiring α] {m : α} {n : α} (hn : m n) (hm : Even m) :
          @[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 : α) :
          @[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 : α) :

          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} [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 α] {m : α} {n : α} :
            Even mOdd nOdd (m + n)
            theorem Even.odd_add {α : Type u_2} [Semiring α] {m : α} {n : α} :
            Even mOdd nOdd (n + m)
            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 Even.add_one {α : Type u_2} [Semiring α] {m : α} (h : Even m) :
            Odd (m + 1)
            @[simp]
            theorem Even.one_add {α : Type u_2} [Semiring α] {m : α} (h : Even m) :
            Odd (1 + m)
            theorem odd_two_mul_add_one {α : Type u_2} [Semiring α] (m : α) :
            Odd (2 * m + 1)
            @[simp]
            theorem odd_add_self_one' {α : Type u_2} [Semiring α] {m : α} :
            Odd (m + (m + 1))
            @[simp]
            theorem odd_add_one_self {α : Type u_2} [Semiring α] {m : α} :
            Odd (m + 1 + m)
            @[simp]
            theorem odd_add_one_self' {α : Type u_2} [Semiring α] {m : α} :
            Odd (m + (1 + m))
            @[simp]
            theorem one_add_self_self {α : Type u_2} [Semiring α] {m : α} :
            Odd (1 + m + m)
            theorem Odd.map {F : Type u_1} {α : Type u_2} {β : Type u_3} [Semiring α] [Semiring β] {m : α} [FunLike F α β] [RingHomClass F α β] (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 α] [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 α] {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 : α} [LinearOrder α] :
            Odd |a| Odd a
            theorem Even.pow_nonneg {R : Type u_4} [LinearOrderedRing R] {n : } (hn : Even n) (a : R) :
            0 a ^ n
            theorem Even.pow_pos {R : Type u_4} [LinearOrderedRing R] {a : R} {n : } (hn : Even n) (ha : a 0) :
            0 < a ^ n
            theorem Odd.pow_nonpos {R : Type u_4} [LinearOrderedRing R] {a : R} {n : } (hn : Odd n) (ha : a 0) :
            a ^ n 0
            theorem Odd.pow_neg {R : Type u_4} [LinearOrderedRing R] {a : R} {n : } (hn : Odd n) (ha : a < 0) :
            a ^ n < 0
            theorem Odd.pow_nonneg_iff {R : Type u_4} [LinearOrderedRing R] {a : R} {n : } (hn : Odd n) :
            0 a ^ n 0 a
            theorem Odd.pow_nonpos_iff {R : Type u_4} [LinearOrderedRing R] {a : R} {n : } (hn : Odd n) :
            a ^ n 0 a 0
            theorem Odd.pow_pos_iff {R : Type u_4} [LinearOrderedRing R] {a : R} {n : } (hn : Odd n) :
            0 < a ^ n 0 < a
            theorem Odd.pow_neg_iff {R : Type u_4} [LinearOrderedRing R] {a : R} {n : } (hn : Odd n) :
            a ^ n < 0 a < 0
            theorem Even.pow_pos_iff {R : Type u_4} [LinearOrderedRing R] {a : R} {n : } (hn : Even n) (h₀ : n 0) :
            0 < a ^ n a 0
            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
            theorem Odd.strictMono_pow {R : Type u_4} [LinearOrderedRing R] {n : } (hn : Odd n) :
            StrictMono fun (a : R) => a ^ n