`BookProof.ChapterF8.twoLevelHash_total` {d k K : ℕ} (h : Fin d → Fin k) (g : Fin k → Fin K) (x : Fin d → ℝ) : twoLevelHash h g x ∈ singleExcitation K

Initializing...

`BookProof.ChapterF8.twoLevelHash_total` {d k K : ℕ} (h : Fin d → Fin k) (g : Fin k → Fin K) (x : Fin d → ℝ) : twoLevelHash h g x ∈ singleExcitation K · Prove2Me