fixes post-merge

Author: Ferinko

ArkLib/Data/CodingTheory.lean

@@ -1,13 +1,11 @@
 import ArkLib.Data.CodingTheory.Basic
 import ArkLib.Data.CodingTheory.BerlekampWelch
-import ArkLib.Data.CodingTheory.BivariatePoly
 import ArkLib.Data.CodingTheory.DivergenceOfSets
 import ArkLib.Data.CodingTheory.InterleavedCode
 import ArkLib.Data.CodingTheory.JohnsonBound
 import ArkLib.Data.CodingTheory.ListDecodability
-import Arklib.Data.CodingTheory.PolishchukSpielman
+import ArkLib.Data.CodingTheory.PolishchukSpielman
 import ArkLib.Data.CodingTheory.Prelims
 import ArkLib.Data.CodingTheory.ProximityGap
-import ArkLib.Data.CodingTheory.PolishchukSpielman
 import ArkLib.Data.CodingTheory.ReedMuller
 import ArkLib.Data.CodingTheory.ReedSolomon

ArkLib/Data/CodingTheory/BivariatePoly.lean

@@ -4,7 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Katerina Hristova, František Silváši, Julian Sutherland
 -/
 
-import ArkLib.Data.CodingTheory.BivariatePoly
+import ArkLib.Data.Polynomial.Bivariate
 
 open Polynomial.Bivariate Polynomial
 

ArkLib/Data/CodingTheory/PolishchukSpielman.lean

@@ -11,6 +11,8 @@ import Mathlib.Data.Fintype.Defs
 open Polynomial
 open Polynomial.Bivariate
 
+namespace Polynomial
+
 namespace Bivariate
 
 noncomputable section
@@ -271,3 +273,5 @@ theorem totalDegree_prod (hf : f ≠ 0) (hg : g ≠ 0) :
 
 end
 end Bivariate
+
+end Polynomial