Documentation

Arithmetization.OmegaOne.Basic

βˆ€ x, βˆƒ y, 2^{|x|^2} = y

Equations
  • One or more equations did not get rendered due to their size.
Instances For
    Equations
    def LO.Arith.hashDef :
    πšΊβ‚€.Semisentence 3
    Equations
    • One or more equations did not get rendered due to their size.
    Instances For
      @[simp]
      theorem LO.Arith.hash_monotone {V : Type u_1} [LO.ORingStruc V] [V βŠ§β‚˜* πˆπšΊβ‚€ + 𝛀₁] {a₁ : V} {aβ‚‚ : V} {b₁ : V} {bβ‚‚ : V} (h₁ : a₁ ≀ b₁) (hβ‚‚ : aβ‚‚ ≀ bβ‚‚) :
      a₁ # aβ‚‚ ≀ b₁ # bβ‚‚
      theorem LO.Arith.hash_two_mul {V : Type u_1} [LO.ORingStruc V] [V βŠ§β‚˜* πˆπšΊβ‚€ + 𝛀₁] (a : V) {b : V} (pos : 0 < b) :
      a # (2 * b) = a # b * a # 1