chore: fixed error in UniPoly by putting Lagrange in namespace

Verified-zkEVM · Dec 20, 2024 · f52f3fc · f52f3fc
1 parent fd1aca9
commit f52f3fc
Showing 1 changed file with 2 additions and 2 deletions.
diff --git a/ZKLib/Data/UniPoly/Basic.lean b/ZKLib/Data/UniPoly/Basic.lean
@@ -298,8 +298,6 @@ def QuotientUniPoly := Quotient (@instSetoidUniPoly R _)
 
 end Equiv
 
-end UniPoly
-
 namespace Lagrange
 
 -- unique polynomial of degree n that has nodes at ω^i for i = 0, 1, ..., n-1
@@ -315,6 +313,8 @@ def interpolate {R : Type*} [Semiring R] (n : ℕ) (ω : R) (r : Vector R n) : U
 
 end Lagrange
 
+end UniPoly
+
 section Tropical
 /-- This section courtesy of Junyan Xu -/