β x, β y, 2^{|x|^2} = y
Equations
- One or more equations did not get rendered due to their size.
Instances For
- omega: πβ LO.Arith.omegaOneAxiom
Instances For
Equations
- LO.Arith.Β«termπβΒ» = Lean.ParserDescr.node `LO.Arith.termπβ 1024 (Lean.ParserDescr.symbol "πβ")
Instances For
@[simp]
theorem
LO.Arith.omegaOne.mem_iff
{Ο : LO.FirstOrder.SyntacticFormula ββα΅£}
:
Ο β πβ β Ο = LO.Arith.omegaOneAxiom
theorem
LO.Arith.models_Omegaβ_iff
{V : Type u_1}
[LO.ORingStruc V]
[V β§β* ππΊβ]
:
V β§β LO.Arith.omegaOneAxiom β β (x : V), β (y : V), LO.Arith.Exponential (βxβ ^ 2) y
instance
LO.Arith.instModelsTheoryHAddTheoryORingISigmaOfNatNatOmegaOne
{V : Type u_1}
[LO.ORingStruc V]
[V β§β* ππΊβ]
:
Equations
- β― = β―
instance
LO.Arith.instModelsTheoryISigmaOfNatNat_arithmetization_1
{V : Type u_1}
[LO.ORingStruc V]
[V β§β* ππΊβ + πβ]
:
Equations
- β― = β―
instance
LO.Arith.instModelsTheoryOmegaOne
{V : Type u_1}
[LO.ORingStruc V]
[V β§β* ππΊβ + πβ]
:
Equations
- β― = β―
theorem
LO.Arith.exists_exponential_sq_length
{V : Type u_1}
[LO.ORingStruc V]
[V β§β* ππΊβ + πβ]
(x : V)
:
β (y : V), LO.Arith.Exponential (βxβ ^ 2) y
theorem
LO.Arith.exists_unique_exponential_sq_length
{V : Type u_1}
[LO.ORingStruc V]
[V β§β* ππΊβ + πβ]
(x : V)
:
β! y : V, LO.Arith.Exponential (βxβ ^ 2) y
theorem
LO.Arith.hash_exists_unique
{V : Type u_1}
[LO.ORingStruc V]
[V β§β* ππΊβ + πβ]
(x : V)
(y : V)
:
instance
LO.Arith.instHash
{V : Type u_1}
[LO.ORingStruc V]
[V β§β* ππΊβ + πβ]
:
Hash V
Equations
- LO.Arith.instHash = { hash := fun (a b : V) => Classical.choose! β― }
theorem
LO.Arith.exponential_hash
{V : Type u_1}
[LO.ORingStruc V]
[V β§β* ππΊβ + πβ]
(a : V)
(b : V)
:
theorem
LO.Arith.exponential_hash_one
{V : Type u_1}
[LO.ORingStruc V]
[V β§β* ππΊβ + πβ]
(a : V)
:
LO.Arith.Exponential βaβ (a # 1)
Equations
- One or more equations did not get rendered due to their size.
Instances For
theorem
LO.Arith.hash_defined
{V : Type u_1}
[LO.ORingStruc V]
[V β§β* ππΊβ + πβ]
:
πΊβ-Functionβ Hash.hash via LO.Arith.hashDef
instance
LO.Arith.hash_definable
{V : Type u_1}
[LO.ORingStruc V]
[V β§β* ππΊβ + πβ]
:
πΊβ-Functionβ Hash.hash
Equations
- β― = β―
@[simp]
theorem
LO.Arith.hash_pow2
{V : Type u_1}
[LO.ORingStruc V]
[V β§β* ππΊβ + πβ]
(a : V)
(b : V)
:
LO.Arith.Pow2 (a # b)
@[simp]
theorem
LO.Arith.hash_pos
{V : Type u_1}
[LO.ORingStruc V]
[V β§β* ππΊβ + πβ]
(a : V)
(b : V)
:
@[simp]
theorem
LO.Arith.hash_lt
{V : Type u_1}
[LO.ORingStruc V]
[V β§β* ππΊβ + πβ]
(a : V)
(b : V)
:
@[simp]
theorem
LO.Arith.hash_zero_left
{V : Type u_1}
[LO.ORingStruc V]
[V β§β* ππΊβ + πβ]
(a : V)
:
@[simp]
theorem
LO.Arith.hash_zero_right
{V : Type u_1}
[LO.ORingStruc V]
[V β§β* ππΊβ + πβ]
(a : V)
:
theorem
LO.Arith.hash_comm
{V : Type u_1}
[LO.ORingStruc V]
[V β§β* ππΊβ + πβ]
(a : V)
(b : V)
:
@[simp]
theorem
LO.Arith.lt_hash_one_right
{V : Type u_1}
[LO.ORingStruc V]
[V β§β* ππΊβ + πβ]
(a : V)
:
@[simp]
theorem
LO.Arith.lt_hash_one_righs
{V : Type u_1}
[LO.ORingStruc V]
[V β§β* ππΊβ + πβ]
(a : V)
:
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β)
:
theorem
LO.Arith.bexp_eq_hash
{V : Type u_1}
[LO.ORingStruc V]
[V β§β* ππΊβ + πβ]
(a : V)
(b : V)
:
theorem
LO.Arith.hash_two_mul
{V : Type u_1}
[LO.ORingStruc V]
[V β§β* ππΊβ + πβ]
(a : V)
{b : V}
(pos : 0 < b)
:
theorem
LO.Arith.hash_two_mul_le_sq_hash
{V : Type u_1}
[LO.ORingStruc V]
[V β§β* ππΊβ + πβ]
(a : V)
(b : V)
: