Documentation

Arithmetization.ISigmaZero.Exponential.Pow2

Equations
Instances For
    Equations
    • One or more equations did not get rendered due to their size.
    Instances For
      Equations
      • β‹― = β‹―
      theorem LO.Arith.Pow2.pos {V : Type u_1} [LO.ORingStruc V] [V βŠ§β‚˜* 𝐈open] {a : V} (h : LO.Arith.Pow2 a) :
      0 < a
      theorem LO.Arith.Pow2.dvd {V : Type u_1} [LO.ORingStruc V] [V βŠ§β‚˜* 𝐈open] {a : V} (h : LO.Arith.Pow2 a) {r : V} (hr : r ≀ a) :
      1 < r β†’ r ∣ a β†’ 2 ∣ r
      theorem LO.Arith.Pow2.two_dvd {V : Type u_1} [LO.ORingStruc V] [V βŠ§β‚˜* 𝐈open] {a : V} (h : LO.Arith.Pow2 a) (lt : 1 < a) :
      2 ∣ a
      theorem LO.Arith.Pow2.two_dvd' {V : Type u_1} [LO.ORingStruc V] [V βŠ§β‚˜* 𝐈open] {a : V} (h : LO.Arith.Pow2 a) (lt : a β‰  1) :
      2 ∣ a
      theorem LO.Arith.Pow2.of_dvd {V : Type u_1} [LO.ORingStruc V] [V βŠ§β‚˜* 𝐈open] {a : V} {b : V} (h : b ∣ a) :
      theorem LO.Arith.Pow2.elim {V : Type u_1} [LO.ORingStruc V] [V βŠ§β‚˜* 𝐈open] {p : V} :
      LO.Arith.Pow2 p ↔ p = 1 ∨ βˆƒ (q : V), p = 2 * q ∧ LO.Arith.Pow2 q
      theorem LO.Arith.Pow2.div_two {V : Type u_1} [LO.ORingStruc V] [V βŠ§β‚˜* 𝐈open] {p : V} (h : LO.Arith.Pow2 p) (ne : p β‰  1) :
      theorem LO.Arith.Pow2.two_mul_div_two {V : Type u_1} [LO.ORingStruc V] [V βŠ§β‚˜* 𝐈open] {p : V} (h : LO.Arith.Pow2 p) (ne : p β‰  1) :
      2 * (p / 2) = p
      theorem LO.Arith.Pow2.div_two_mul_two {V : Type u_1} [LO.ORingStruc V] [V βŠ§β‚˜* 𝐈open] {p : V} (h : LO.Arith.Pow2 p) (ne : p β‰  1) :
      p / 2 * 2 = p
      theorem LO.Arith.Pow2.elim' {V : Type u_1} [LO.ORingStruc V] [V βŠ§β‚˜* 𝐈open] {p : V} :
      LO.Arith.Pow2 p ↔ p = 1 ∨ 1 < p ∧ βˆƒ (q : V), p = 2 * q ∧ LO.Arith.Pow2 q
      def LO.Arith.LenBit {V : Type u_1} [LO.ORingStruc V] [V βŠ§β‚˜* 𝐈open] (i : V) (a : V) :

      $\mathrm{LenBit} (2^i, a) \iff \text{$i$th-bit of $a$ is $1$}$.

      Equations
      Instances For
        Equations
        • One or more equations did not get rendered due to their size.
        Instances For
          Equations
          • β‹― = β‹―
          theorem LO.Arith.LenBit.le {V : Type u_1} [LO.ORingStruc V] [V βŠ§β‚˜* 𝐈open] {i : V} {a : V} (h : LO.Arith.LenBit i a) :
          theorem LO.Arith.not_lenbit_of_lt {V : Type u_1} [LO.ORingStruc V] [V βŠ§β‚˜* 𝐈open] {i : V} {a : V} (h : a < i) :
          theorem LO.Arith.LenBit.iff_rem {V : Type u_1} [LO.ORingStruc V] [V βŠ§β‚˜* 𝐈open] {i : V} {a : V} :
          LO.Arith.LenBit i a ↔ a / i % 2 = 1
          @[simp]
          theorem LO.Arith.LenBit.self {V : Type u_1} [LO.ORingStruc V] [V βŠ§β‚˜* 𝐈open] {a : V} (pos : 0 < a) :
          theorem LO.Arith.LenBit.mod {V : Type u_1} [LO.ORingStruc V] [V βŠ§β‚˜* 𝐈open] {i : V} {a : V} {k : V} (h : 2 * i ∣ k) :
          theorem LO.Arith.LenBit.add {V : Type u_1} [LO.ORingStruc V] [V βŠ§β‚˜* 𝐈open] {i : V} {a : V} {b : V} (h : 2 * i ∣ b) :
          theorem LO.Arith.LenBit.add_self {V : Type u_1} [LO.ORingStruc V] [V βŠ§β‚˜* 𝐈open] {i : V} {a : V} (h : a < i) :
          theorem LO.Arith.LenBit.add_self_of_lenbit {V : Type u_1} [LO.ORingStruc V] [V βŠ§β‚˜* 𝐈open] {a : V} {i : V} (pos : 0 < i) (h : LO.Arith.LenBit i a) :
          theorem LO.Arith.LenBit.sub_self_of_lenbit {V : Type u_1} [LO.ORingStruc V] [V βŠ§β‚˜* 𝐈open] {a : V} {i : V} (pos : 0 < i) (h : LO.Arith.LenBit i a) :
          theorem LO.Arith.Pow2.dvd_of_le {V : Type u_1} [LO.ORingStruc V] [V βŠ§β‚˜* πˆπšΊβ‚€] {a : V} {b : V} (ha : LO.Arith.Pow2 a) (hb : LO.Arith.Pow2 b) :
          a ≀ b β†’ a ∣ b
          theorem LO.Arith.Pow2.sq_or_dsq {V : Type u_1} [LO.ORingStruc V] [V βŠ§β‚˜* πˆπšΊβ‚€] {a : V} (pa : LO.Arith.Pow2 a) :
          βˆƒ (b : V), a = b ^ 2 ∨ a = 2 * b ^ 2
          theorem LO.Arith.Pow2.mul_add_lt_of_mul_lt_of_pos {V : Type u_1} [LO.ORingStruc V] [V βŠ§β‚˜* πˆπšΊβ‚€] {a : V} {b : V} {p : V} {q : V} (hp : LO.Arith.Pow2 p) (hq : LO.Arith.Pow2 q) (h : a * p < q) (hb : b < p) (hbq : b < q) :
          a * p + b < q
          theorem LO.Arith.LenBit.mod_pow2 {V : Type u_1} [LO.ORingStruc V] [V βŠ§β‚˜* πˆπšΊβ‚€] {a : V} {i : V} {j : V} (pi : LO.Arith.Pow2 i) (pj : LO.Arith.Pow2 j) (h : i < j) :
          theorem LO.Arith.LenBit.add_pow2 {V : Type u_1} [LO.ORingStruc V] [V βŠ§β‚˜* πˆπšΊβ‚€] {a : V} {i : V} {j : V} (pi : LO.Arith.Pow2 i) (pj : LO.Arith.Pow2 j) (h : i < j) :
          theorem LO.Arith.lenbit_iff_add_mul {V : Type u_1} [LO.ORingStruc V] [V βŠ§β‚˜* πˆπšΊβ‚€] {i : V} {a : V} (hi : LO.Arith.Pow2 i) :
          LO.Arith.LenBit i a ↔ βˆƒ (k : V), βˆƒ r < i, a = k * (2 * i) + i + r
          theorem LO.Arith.not_lenbit_iff_add_mul {V : Type u_1} [LO.ORingStruc V] [V βŠ§β‚˜* πˆπšΊβ‚€] {i : V} {a : V} (hi : LO.Arith.Pow2 i) :
          Β¬LO.Arith.LenBit i a ↔ βˆƒ (k : V), βˆƒ r < i, a = k * (2 * i) + r
          theorem LO.Arith.lenbit_mul_add {V : Type u_1} [LO.ORingStruc V] [V βŠ§β‚˜* πˆπšΊβ‚€] {i : V} {j : V} {a : V} {r : V} (pi : LO.Arith.Pow2 i) (pj : LO.Arith.Pow2 j) (hr : r < j) :