diff --git a/ZKLib/Data/UniPoly/Basic.lean b/ZKLib/Data/UniPoly/Basic.lean
index 99f47c5..e3ddc21 100644
--- 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 -/