Documentation

Arithmetization.OmegaOne.Basic

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

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