Basics of Coding Theory

We define a general code C to be a subset of n → R for some finite index set n and some target type R.

We can then specialize this notion to various settings. For [CommSemiring R], we define a linear code to be a linear subspace of n → R. We also define the notion of generator matrix and (parity) check matrix.

Main Definitions

• codeDist C: The Hamming distance of a code C, defined as the infimum (in ℕ∞) of the Hamming distances between any two distinct elements of C. This is noncomputable.

• codeDist' C: A computable version of codeDist C, assuming C is a Fintype.

We define the block length, rate, and distance of C. We prove simple properties of linear codes such as the singleton bound.

def Distance.«termΔ₀(_,_)» : Lean.ParserDescr

Equations

• One or more equations did not get rendered due to their size.

def Distance.«term‖_‖₀» : Lean.ParserDescr

Equations

• One or more equations did not get rendered due to their size.

noncomputable def Distance.codeDist {n : Type u_1} [Fintype n] {R : Type u_2} [DecidableEq R] (C : Set (n → R)) : ℕ

The Hamming distance of a code C is the minimum Hamming distance between any two distinct elements of the code. cd We formalize this as the infimum sInf over all d : ℕ such that there exist u v : n → R in the code with u ≠ v and hammingDist u v ≤ d. If none exists, then we define the distance to be 0.

Equations

• ‖C‖₀ = sInf {d : ℕ | ∃ u ∈ C, ∃ v ∈ C, u ≠ v ∧ Δ₀(u, v) ≤ d}

instance Distance.instEDistForall_arkLib {n : Type u_1} [Fintype n] {R : Type u_2} [DecidableEq R] : EDist (n → R)

Equations

• Distance.instEDistForall_arkLib = { edist := fun (u v : n → R) => ↑Δ₀(u, v) }

instance Distance.instDistForall_arkLib {n : Type u_1} [Fintype n] {R : Type u_2} [DecidableEq R] : Dist (n → R)

Equations

• Distance.instDistForall_arkLib = { dist := fun (u v : n → R) => ↑Δ₀(u, v) }

noncomputable def Distance.eCodeDistNew {n : Type u_1} [Fintype n] {R : Type u_2} [DecidableEq R] (C : Set (n → R)) : ENNReal

Equations

• Distance.eCodeDistNew C = C.einfsep

noncomputable def Distance.codeDistNew {n : Type u_1} [Fintype n] {R : Type u_2} [DecidableEq R] (C : Set (n → R)) : ℝ

Equations

• Distance.codeDistNew C = C.infsep

def Distance.«term‖_‖₀_1» : Lean.ParserDescr

Equations

• One or more equations did not get rendered due to their size.

noncomputable def Distance.distFromCode {n : Type u_1} [Fintype n] {R : Type u_2} [DecidableEq R] (u : n → R) (C : Set (n → R)) : ℕ∞

The distance from a vector u to a code C is the minimum Hamming distance between u and any element of C.

Equations

• Δ₀(u, C) = sInf {d : ℕ∞ | ∃ v ∈ C, ↑Δ₀(u, v) ≤ d}

def Distance.«termΔ₀(_,_)_1» : Lean.ParserDescr

Equations

• One or more equations did not get rendered due to their size.

noncomputable def Distance.minDist {n : Type u_1} [Fintype n] {R : Type u_2} [DecidableEq R] (C : Set (n → R)) : ℕ

Equations

• Distance.minDist C = sInf {d : ℕ | ∃ u ∈ C, ∃ v ∈ C, u ≠ v ∧ Δ₀(u, v) = d}

@[simp]

theorem Distance.codeDist_empty {n : Type u_1} [Fintype n] {R : Type u_2} [DecidableEq R] : ‖∅‖₀ = 0

@[simp]

theorem Distance.codeDist_subsingleton {n : Type u_1} [Fintype n] {R : Type u_2} [DecidableEq R] {C : Set (n → R)} [Subsingleton ↑C] : ‖C‖₀ = 0

@[simp]

theorem Distance.codeDist_le_card {n : Type u_1} [Fintype n] {R : Type u_2} [DecidableEq R] (C : Set (n → R)) : ‖C‖₀ ≤ Fintype.card n

theorem Distance.eq_of_lt_codeDist {n : Type u_1} [Fintype n] {R : Type u_2} [DecidableEq R] {C : Set (n → R)} {u v : n → R} (hu : u ∈ C) (hv : v ∈ C) (huv : Δ₀(u, v) < ‖C‖₀) : u = v

If u and v are two codewords of C with distance less than codeDist C, then they are the same.

@[simp]

theorem Distance.distFromCode_of_empty {n : Type u_1} [Fintype n] {R : Type u_2} [DecidableEq R] (u : n → R) : Δ₀(u, ∅) = ⊤

theorem Distance.distFromCode_eq_top_iff_empty {n : Type u_1} [Fintype n] {R : Type u_2} [DecidableEq R] (u : n → R) (C : Set (n → R)) : Δ₀(u, C) = ⊤ ↔ C = ∅

@[simp]

theorem Distance.distFromCode_of_mem {n : Type u_1} [Fintype n] {R : Type u_2} [DecidableEq R] (C : Set (n → R)) {u : n → R} (h : u ∈ C) : Δ₀(u, C) = 0

theorem Distance.distFromCode_eq_zero_iff_mem {n : Type u_1} [Fintype n] {R : Type u_2} [DecidableEq R] (C : Set (n → R)) (u : n → R) : Δ₀(u, C) = 0 ↔ u ∈ C

theorem Distance.distFromCode_eq_of_lt_half_codeDist {n : Type u_1} [Fintype n] {R : Type u_2} [DecidableEq R] (C : Set (n → R)) (u : n → R) {v w : n → R} (hv : v ∈ C) (hw : w ∈ C) (huv : Δ₀(u, v) < ‖C‖₀ / 2) (hvw : Δ₀(u, w) < ‖C‖₀ / 2) : v = w

def Distance.codeDist' {n : Type u_1} [Fintype n] {R : Type u_2} [DecidableEq R] (C : Set (n → R)) [Fintype ↑C] : ℕ∞

Computable version of the Hamming distance of a code C, assuming C is a Fintype.

The return type is ℕ∞ since we use Finset.min.

Equations

• ‖C‖₀' = (Finset.image (fun (x : ↑C × ↑C) => match x with | (u, v) => Δ₀(↑u, ↑v)) {p : ↑C × ↑C | p.1 ≠ p.2}).min

def Distance.«term‖_‖₀'» : Lean.ParserDescr

Equations

• One or more equations did not get rendered due to their size.

@[simp]

theorem Distance.codeDist'_empty {n : Type u_1} [Fintype n] {R : Type u_2} [DecidableEq R] : ‖∅‖₀' = ⊤

@[simp]

theorem Distance.codeDist'_subsingleton {n : Type u_1} [Fintype n] {R : Type u_2} [DecidableEq R] {C : Set (n → R)} [Fintype ↑C] [Subsingleton ↑C] : ‖C‖₀' = ⊤

theorem Distance.codeDist'_eq_codeDist {n : Type u_1} [Fintype n] {R : Type u_2} [DecidableEq R] {C : Set (n → R)} [Fintype ↑C] : ‖C‖₀'.toNat = ‖C‖₀

def Distance.possibleDistsToC {α : Type u_3} {F : Type u_4} {ι : Type u_5} (w : ι → F) (C : Set (ι → F)) (δf : (ι → F) → (ι → F) → α) : Set α

The set of possible distances δf from a vector w to a code C.

Equations

• Distance.possibleDistsToC w C δf = {d : α | ∃ c ∈ C, c ≠ w ∧ δf w c = d}

def Distance.possibleDists {α : Type u_3} {F : Type u_4} {ι : Type u_5} (C : Set (ι → F)) (δf : (ι → F) → (ι → F) → α) : Set α

The set of possible distances δf between distinct codewords in a code C.

• TODO: This allows us to express distance in non-ℝ, which is quite convenient. Extending to (E)Dist forces this into ℝ; give some thought.

Equations

• Distance.possibleDists C δf = {d : α | ∃ p ∈ C.offDiag, δf p.1 p.2 = d}

noncomputable def Distance.distToCode {α : Type u_3} {F : Type u_4} {ι : Type u_5} [LinearOrder α] [Zero α] (w : ι → F) (C : Set (ι → F)) (δf : (ι → F) → (ι → F) → α) (h : (possibleDistsToC w C δf).Finite) : WithTop α

A generalisation of distFromCode for an arbitrary distance function δf.

Equations

• Distance.distToCode w C δf h = (Distance.possibleDistsToC w C δf).toFinset.min

theorem Distance.distToCode_of_nonempty {α : Type u_3} [LinearOrder α] [Zero α] {ι : Type u_4} {F : Type u_5} {w : ι → F} {C : Set (ι → F)} {δf : (ι → F) → (ι → F) → α} (h₁ : (possibleDistsToC w C δf).Finite) (h₂ : (possibleDistsToC w C δf).Nonempty) : distToCode w C δf h₁ = ↑((possibleDistsToC w C δf).toFinset.min' ⋯)

def Distance.distFromCode' {n : Type u_1} [Fintype n] {R : Type u_2} [DecidableEq R] (C : Set (n → R)) [Fintype ↑C] (u : n → R) : ℕ∞

Computable version of the distance from a vector u to a code C, assuming C is a Fintype.

Equations

• Δ₀'(u, C) = (Finset.image (fun (v : ↑C) => Δ₀(u, ↑v)) Finset.univ).min

def Distance.«termΔ₀'(_,_)» : Lean.ParserDescr

Equations

• One or more equations did not get rendered due to their size.

def codeByGenMatrix {n : Type u_1} {R : Type u_2} {k : Type u_3} [Fintype k] [CommSemiring R] (G : Matrix k n R) : Submodule R (n → R)

Define a linear code from its generator matrix

Equations

• codeByGenMatrix G = LinearMap.range G.vecMulLinear

def codeByCheckMatrix {n : Type u_1} [Fintype n] {R : Type u_2} {k : Type u_3} [CommSemiring R] (H : Matrix k n R) : Submodule R (n → R)

Define a linear code from its (parity) check matrix

Equations

• codeByCheckMatrix H = LinearMap.ker H.mulVecLin

noncomputable def linearCodeDist {n : Type u_1} [Fintype n] {R : Type u_2} [DecidableEq R] [CommSemiring R] (C : Submodule R (n → R)) : ℕ

The Hamming distance of a linear code can also be defined as the minimum Hamming norm of a non-zero vector in the code

Equations

• linearCodeDist C = sInf {d : ℕ | ∃ u ∈ C, u ≠ 0 ∧ ‖u‖₀ ≤ d}

theorem codeDist_eq_linearCodeDist {n : Type u_1} [Fintype n] {R : Type u_2} [DecidableEq R] [CommSemiring R] (C : Submodule R (n → R)) : ‖C.carrier‖₀ = linearCodeDist C

def linearCodeDist' {n : Type u_1} [Fintype n] {R : Type u_2} [DecidableEq R] [CommSemiring R] [DecidableEq n] [Fintype R] (C : Submodule R (n → R)) [DecidablePred fun (x : n → R) => x ∈ C] : ℕ∞

A computable version of the Hamming distance of a linear code C.

Equations

• linearCodeDist' C = (Finset.image (fun (v : ↥C) => ‖↑v‖₀) {v : ↥C | v ≠ 0}).min

def interleaveCode {n : Type u_1} {R : Type u_2} [CommSemiring R] (C : Submodule R (n → R)) (ι : Type u_4) : Submodule R (ι × n → R)

The interleaving of a linear code C over index set ι is the submodule spanned by ι × n-matrices whose rows are elements of C.

Equations

• (C^⋈ι) = Submodule.span R {v : ι × n → R | ∀ (i : ι), ∃ c ∈ C, c = fun (j : n) => v (i, j)}

def «term_^⋈_» : Lean.TrailingParserDescr

Equations

• «term_^⋈_» = Lean.ParserDescr.trailingNode `«term_^⋈_» 20 0 (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.symbol "^⋈") (Lean.ParserDescr.cat `term 0))

def Function.interleave₂ {α : Type u_4} {β : Type u_5} (u v : α → β) : Fin 2 × α → β

Interleave two functions u v : α → β.

Equations

• (u⋈v) = Function.uncurry fun (a : Fin 2) => if a = 0 then u else v

def «term_⋈_» : Lean.TrailingParserDescr

Equations

• «term_⋈_» = Lean.ParserDescr.trailingNode `«term_⋈_» 20 0 (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.symbol "⋈") (Lean.ParserDescr.cat `term 0))

def projection {n : Type u_1} {R : Type u_2} (S : Finset n) (w : n → R) : { x : n // x ∈ S } → R

Equations

• projection S w i = w ↑i

theorem projection_injective {n : Type u_1} [Fintype n] {R : Type u_2} [DecidableEq R] (C : Set (n → R)) (nontriv : ‖C‖₀ ≥ 1) (S : Finset n) (hS : Fintype.card { x : n // x ∈ S } = Fintype.card n - (‖C‖₀ - 1)) (u v : n → R) (hu : u ∈ C) (hv : v ∈ C) : projection S u = projection S v → u = v

theorem singleton_bound {n : Type u_1} [Fintype n] {R : Type u_2} [DecidableEq R] [Finite R] (C : Set (n → R)) : Fintype.card ↑C ≤ Fintype.card R ^ (Fintype.card n - (‖C‖₀ - 1))

Singleton bound for arbitrary codes

theorem singleton_bound_linear {n : Type u_1} [Fintype n] {R : Type u_2} [DecidableEq R] [Finite R] [DivisionRing R] (C : Submodule R (n → R)) : Module.finrank R ↥C ≤ Fintype.card n - ‖C.carrier‖₀ + 1

Singleton bound for linear codes

def RelativeHamming.dist {ι : Type u_3} [Fintype ι] {F : Type u_4} [DecidableEq F] (u v : ι → F) : ℚ

Equations

• δᵣ(u, v) = ↑Δ₀(u, v) / ↑(Fintype.card ι)

def RelativeHamming.«termδᵣ(_,_)» : Lean.ParserDescr

δᵣ(u,v) denotes the relative Hamming distance between vectors u and v.

Equations

• One or more equations did not get rendered due to their size.

@[simp]

theorem RelativeHamming.relHammingDist_le_one {ι : Type u_3} [Fintype ι] {F : Type u_4} {u v : ι → F} [Nonempty ι] [DecidableEq F] : δᵣ(u, v) ≤ 1

The relative Hamming distance between two vectors is at most 1.

@[simp]

theorem RelativeHamming.zero_le_relHammingDist {ι : Type u_3} [Fintype ι] {F : Type u_4} {u v : ι → F} [Nonempty ι] [DecidableEq F] : 0 ≤ δᵣ(u, v)

The relative Hamming distance between two vectors is non-negative.

def RelativeHamming.relHammingDistRange (ι : Type u_5) [Fintype ι] : Set ℚ

The range of the relative Hamming distance function.

Equations

• RelativeHamming.relHammingDistRange ι = {d : ℚ | ∃ d' ≤ Fintype.card ι, d = ↑d' / ↑(Fintype.card ι)}

@[simp]

theorem RelativeHamming.relHammingDist_mem_relHammingDistRange {ι : Type u_3} [Fintype ι] {F : Type u_4} {u v : ι → F} [DecidableEq F] : δᵣ(u, v) ∈ relHammingDistRange ι

The range of the relative Hamming distance is well-defined.

@[simp]

theorem RelativeHamming.finite_relHammingDistRange {ι : Type u_3} [Fintype ι] [Nonempty ι] : (relHammingDistRange ι).Finite

The range of the relative Hamming distance function is finite.

@[simp]

theorem RelativeHamming.finite_offDiag {ι : Type u_3} [Fintype ι] {F : Type u_4} {C : Set (ι → F)} [Finite F] : C.offDiag.Finite

The set of pairs of distinct elements from a finite set is finite.

def RelativeHamming.possibleDists {ι : Type u_3} [Fintype ι] {F : Type u_4} [DecidableEq F] (C : Set (ι → F)) : Set ℚ

The set of possible distances between distinct codewords in a code.

Equations

• RelativeHamming.possibleDists C = Distance.possibleDists C RelativeHamming.dist

@[simp]

theorem RelativeHamming.possibleDists_subset_relHammingDistRange {ι : Type u_3} [Fintype ι] {F : Type u_4} {C : Set (ι → F)} [DecidableEq F] : possibleDists C ⊆ relHammingDistRange ι

The set of possible distances between distinct codewords in a code is a subset of the range of the relative Hamming distance function.

@[simp]

theorem RelativeHamming.finite_possibleDists {ι : Type u_3} [Fintype ι] {F : Type u_4} {C : Set (ι → F)} [DecidableEq F] [Nonempty ι] : (possibleDists C).Finite

The set of possible distances between distinct codewords in a code is a finite set.

def RelativeHamming.minRelHammingDistCode {ι : Type u_3} [Fintype ι] {F : Type u_4} [DecidableEq F] [Nonempty ι] (C : Set (ι → F)) : ℚ

The minimum relative Hamming distance of a code.

Equations

• (δᵣ C) = if h : (RelativeHamming.possibleDists C).Nonempty then (RelativeHamming.possibleDists C).toFinset.min' ⋯ else 0

def RelativeHamming.termδᵣ_ : Lean.ParserDescr

δᵣ C denotes the minimum relative Hamming distance of a code C.

Equations

• RelativeHamming.termδᵣ_ = Lean.ParserDescr.node `RelativeHamming.termδᵣ_ 1022 (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.symbol "δᵣ") (Lean.ParserDescr.cat `term 0))

@[simp]

theorem RelativeHamming.possibleDistsToC_subset_relHammingDistRange {ι : Type u_3} [Fintype ι] {F : Type u_4} {w : ι → F} {C : Set (ι → F)} [DecidableEq F] : Distance.possibleDistsToC w C dist ⊆ relHammingDistRange ι

The range set of possible relative Hamming distances from a vector to a code is a subset of the range of the relative Hamming distance function.

@[simp]

theorem RelativeHamming.finite_possibleDistsToC {ι : Type u_3} [Fintype ι] {F : Type u_4} {w : ι → F} {C : Set (ι → F)} [Nonempty ι] [DecidableEq F] : (Distance.possibleDistsToC w C dist).Finite

The set of possible relative Hamming distances from a vector to a code is a finite set.

instance RelativeHamming.instFintypeElemRatPossibleDistsToCDistOfNonempty {ι : Type u_3} [Fintype ι] {F : Type u_4} {w : ι → F} {C : Set (ι → F)} [Nonempty ι] [DecidableEq F] : Fintype ↑(Distance.possibleDistsToC w C dist)

Equations

• RelativeHamming.instFintypeElemRatPossibleDistsToCDistOfNonempty = Fintype.ofFinite ↑(Distance.possibleDistsToC w C RelativeHamming.dist)

def RelativeHamming.relHammingDistToCode {ι : Type u_3} [Fintype ι] {F : Type u_4} [Nonempty ι] [DecidableEq F] (w : ι → F) (C : Set (ι → F)) : ℚ

The relative Hamming distance from a vector to a code.

Equations

• δᵣ(w, C) = if h : (Distance.possibleDistsToC w C RelativeHamming.dist).Nonempty then Option.get (Distance.distToCode w C RelativeHamming.dist ⋯) ⋯ else 0

theorem RelativeHamming.relHammingDistToCode.p {ι : Type u_3} [Fintype ι] {F : Type u_4} [Nonempty ι] [DecidableEq F] (w : ι → F) (C : Set (ι → F)) (h : (Distance.possibleDistsToC w C dist).Nonempty) : Option.isSome (Distance.distToCode w C dist ⋯) = true

def RelativeHamming.«termδᵣ(_,_)_1» : Lean.ParserDescr

δᵣ(w,C) denotes the relative Hamming distance between a vector w and a code C.

Equations

• One or more equations did not get rendered due to their size.

@[simp]

theorem RelativeHamming.zero_mem_relHammingDistRange {ι : Type u_3} [Fintype ι] : 0 ∈ relHammingDistRange ι

@[simp]

theorem RelativeHamming.relHammingDistToCode_mem_relHammingDistRange {ι : Type u_3} [Fintype ι] {F : Type u_4} {c : ι → F} {C : Set (ι → F)} [Nonempty ι] [DecidableEq F] : δᵣ(c, C) ∈ relHammingDistRange ι

The relative Hamming distances between a vector and a codeword is in the range of the relative Hamming distance function.

@[reducible, inline]

abbrev LinearCode (ι : Type u) [Fintype ι] (F : Type v) [Semiring F] : Type (max u v)

Equations

• LinearCode ι F = Submodule F (ι → F)

noncomputable def LinearCode.wt {F : Type u_3} {ι : Type u_4} [Fintype ι] [DecidableEq F] [Zero F] (v : ι → F) : ℕ

Equations

• LinearCode.wt v = {i : ι | v i ≠ 0}.card

theorem LinearCode.wt_eq_zero_iff {F : Type u_3} {ι : Type u_4} [Fintype ι] [DecidableEq F] [Zero F] {v : ι → F} : wt v = 0 ↔ Fintype.card ι = 0 ∨ ∀ (i : ι), v i = 0

def LinearCode.fromRowGenMat {F : Type u_3} {ι : Type u_5} [Fintype ι] {κ : Type u_6} [Fintype κ] [Semiring F] (G : Matrix κ ι F) : LinearCode ι F

Linear code defined by left multiplication by its generator matrix.

Equations

• LinearCode.fromRowGenMat G = LinearMap.range G.vecMulLinear

def LinearCode.fromColGenMat {F : Type u_3} {ι : Type u_5} [Fintype ι] {κ : Type u_6} [Fintype κ] [CommRing F] (G : Matrix ι κ F) : LinearCode ι F

Linear code defined by right multiplication by a generator matrix.

Equations

• LinearCode.fromColGenMat G = LinearMap.range G.mulVecLin

noncomputable def LinearCode.dim {F : Type u_3} {ι : Type u_5} [Fintype ι] [Semiring F] (LC : LinearCode ι F) : ℕ

Equations

• LC.dim = Module.finrank F ↥LC

theorem LinearCode.rank_eq_dim_fromColGenMat {F : Type u_3} {ι : Type u_5} [Fintype ι] {κ : Type u_6} [Fintype κ] [CommRing F] {G : Matrix κ ι F} : G.rank = (fromColGenMat G).dim

The dimension of a linear code equals the rank of its associated generator matrix.

def LinearCode.length {F : Type u_3} {ι : Type u_5} [Fintype ι] [Semiring F] : LinearCode ι F → ℕ

Equations

• x✝.length = Fintype.card ι

noncomputable def LinearCode.rate {F : Type u_3} {ι : Type u_5} [Fintype ι] [Semiring F] (LC : LinearCode ι F) : ℚ

Equations

• (ρ LC) = ↑LC.dim / ↑LC.length

def LinearCode.termρ_ : Lean.ParserDescr

ρ LC is the rate of the linear code LC.

Equations

• LinearCode.termρ_ = Lean.ParserDescr.node `LinearCode.termρ_ 1022 (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.symbol "ρ") (Lean.ParserDescr.cat `term 0))

noncomputable def LinearCode.minWtCodewords {F : Type u_3} {ι : Type u_5} [Fintype ι] [DecidableEq F] [Semiring F] (LC : LinearCode ι F) : ℕ

The minimum taken over the weight of codewords in a linear code.

Equations

• LC.minWtCodewords = sInf {w : ℕ | ∃ c ∈ LC, c ≠ 0 ∧ LinearCode.wt c = w}

theorem LinearCode.hammingDist_eq_wt_sub {F : Type u_3} {ι : Type u_5} [Fintype ι] [DecidableEq F] [CommRing F] {u v : ι → F} : Δ₀(u, v) = wt (u - v)

The Hamming distance between codewords equals to the weight of their difference.

theorem LinearCode.minDist_eq_minWtCodewords {F : Type u_3} {ι : Type u_5} [Fintype ι] [DecidableEq F] [CommRing F] {LC : LinearCode ι F} : Distance.minDist ↑LC = LC.minWtCodewords

The min distance of a linear code equals to the minimum of the weights of non-zero codewords.

theorem LinearCode.minDist_UB {F : Type u_3} {ι : Type u_5} [Fintype ι] [DecidableEq F] [CommRing F] {LC : LinearCode ι F} : Distance.minDist ↑LC ≤ LC.length

theorem LinearCode.singletonBound {F : Type u_3} {ι : Type u_5} [Fintype ι] [DecidableEq F] [Semiring F] (LC : LinearCode ι F) : LC.dim ≤ LC.length - Distance.minDist ↑LC + 1

theorem poly_eq_zero_of_dist_lt {n k : ℕ} {F : Type u_3} [DecidableEq F] [CommRing F] [IsDomain F] {p : Polynomial F} {ωs : Fin n → F} (h_deg : p.natDegree < k) (hn : k ≤ n) (h_inj : Function.Injective ωs) (h_dist : Δ₀((fun (a : F) => Polynomial.eval a p) ∘ ωs, 0) < n - k + 1) : p = 0