Fixed imports

Author: Julek

ArkLib/Data/CodingTheory.lean

@@ -1,6 +1,5 @@
 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.ListDecodability

ArkLib/Data/CodingTheory/BivariatePoly.lean

@@ -27,7 +27,7 @@ The set of coefficients of a bivariate polynomial.
 def coeffs : Finset F[X] := f.support.image (fun n => f.coeff n)
 
 /---
-The coeffiecient of `Y^n` is a polynomial in `X`.
+The coefficient of `Y^n` is a polynomial in `X`.
 -/
 def coeff_Y_n (n : ℕ) : F[X] := f.coeff n
 
@@ -59,7 +59,7 @@ classical sense if the bivariate polynomial is interpreted as a univariate polyn
 def leadingCoeffY : F[X] := f.coeff (natDegree f)
 
 /--
-The polynomial coeffient of the highest power of `Y` is `0` if and only if the bivariate
+The polynomial coefficient of the highest power of `Y` is `0` if and only if the bivariate
 polynomial is the zero polynomial.
 -/
 theorem leadingCoeffY_eq_zero : leadingCoeffY f = 0 ↔ f = 0 :=
@@ -69,7 +69,7 @@ theorem leadingCoeffY_eq_zero : leadingCoeffY f = 0 ↔ f = 0 :=
     fun h => h.symm ▸ leadingCoeff_zero⟩
 
 /--
-The polynomial coeffient of the highest power of `Y` is not `0` if and only if the
+The polynomial coefficient of the highest power of `Y` is not `0` if and only if the
 bivariate polynomial is non-zero.
 -/
 lemma ne_zero_iff_leadingCoeffY_ne_zero : leadingCoeffY f ≠ 0 ↔ f ≠ 0 := by