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

• dist 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.

• dist' C: A computable version of dist 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 Code.«termΔ₀(_,_)» : Lean.ParserDescr

Equations

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

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

Equations

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

noncomputable def Code.dist {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 Code.instEDistForall_arkLib {n : Type u_1} [Fintype n] {R : Type u_2} [DecidableEq R] : EDist (n → R)

Equations

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

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

Equations

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

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

Equations

• Code.eCodeDistNew C = C.einfsep

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

Equations

• Code.codeDistNew C = C.infsep

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

Equations

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

noncomputable def Code.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 Code.«termΔ₀(_,_)_1» : Lean.ParserDescr

Equations

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

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

Equations

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

@[simp]

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

@[simp]

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

@[simp]

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

theorem Code.eq_of_lt_dist {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 dist C, then they are the same.

@[simp]

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

theorem Code.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 Code.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 Code.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 Code.distFromCode_eq_of_lt_half_dist {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 Code.dist' {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 Code.«term‖_‖₀'» : Lean.ParserDescr

Equations

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

@[simp]

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

@[simp]

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

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

def Code.possibleDistsToCode {α : 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

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

def Code.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

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

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

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

Equations

• Code.distToCode w C δf h = (Code.possibleDistsToCode w C δf).toFinset.min

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

def Code.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 Code.«termΔ₀'(_,_)» : Lean.ParserDescr

Equations

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

def Code.relHammingDist {ι : Type u_3} [Fintype ι] {F : Type u_4} [DecidableEq F] (u v : ι → F) : ℚ≥0

Equations

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

def Code.«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 Code.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 Code.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 Code.relHammingDistRange (ι : Type u_5) [Fintype ι] : Set ℚ≥0

The range of the relative Hamming distance function.

Equations

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

@[simp]

theorem Code.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 Code.finite_relHammingDistRange {ι : Type u_3} [Fintype ι] [Nonempty ι] : (relHammingDistRange ι).Finite

The range of the relative Hamming distance function is finite.

@[simp]

theorem Code.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 Code.possibleRelHammingDists {ι : Type u_3} [Fintype ι] {F : Type u_4} [DecidableEq F] (C : Set (ι → F)) : Set ℚ≥0

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

Equations

• Code.possibleRelHammingDists C = Code.possibleDists C Code.relHammingDist

@[simp]

theorem Code.possibleRelHammingDists_subset_relHammingDistRange {ι : Type u_3} [Fintype ι] {F : Type u_4} {C : Set (ι → F)} [DecidableEq F] : possibleRelHammingDists 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 Code.finite_possibleRelHammingDists {ι : Type u_3} [Fintype ι] {F : Type u_4} {C : Set (ι → F)} [DecidableEq F] [Nonempty ι] : (possibleRelHammingDists C).Finite

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

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

The minimum relative Hamming distance of a code.

Equations

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

def Code.termδᵣ_ : Lean.ParserDescr

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

Equations

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

@[simp]

theorem Code.possibleRelHammingDistsToC_subset_relHammingDistRange {ι : Type u_3} [Fintype ι] {F : Type u_4} {w : ι → F} {C : Set (ι → F)} [DecidableEq F] : possibleDistsToCode w C relHammingDist ⊆ 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 Code.finite_possibleRelHammingDistsToCode {ι : Type u_3} [Fintype ι] {F : Type u_4} {w : ι → F} {C : Set (ι → F)} [Nonempty ι] [DecidableEq F] : (possibleDistsToCode w C relHammingDist).Finite

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

instance Code.instFintypeElemNNRatPossibleDistsToCodeRelHammingDistOfNonempty {ι : Type u_3} [Fintype ι] {F : Type u_4} {w : ι → F} {C : Set (ι → F)} [Nonempty ι] [DecidableEq F] : Fintype ↑(possibleDistsToCode w C relHammingDist)

Equations

• Code.instFintypeElemNNRatPossibleDistsToCodeRelHammingDistOfNonempty = Fintype.ofFinite ↑(Code.possibleDistsToCode w C Code.relHammingDist)

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

The relative Hamming distance from a vector to a code.

Equations

• δᵣ(w, C) = if h : (Code.possibleDistsToCode w C Code.relHammingDist).Nonempty then Option.get (Code.distToCode w C Code.relHammingDist ⋯) ⋯ else 0

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

def Code.«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 Code.zero_mem_relHammingDistRange {ι : Type u_3} [Fintype ι] : 0 ∈ relHammingDistRange ι

@[simp]

theorem Code.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.

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

Equations

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

theorem Code.wt_eq_hammingNorm {F : Type u_3} [DecidableEq F] {ι : Type u_4} [Fintype ι] [Zero F] {v : ι → F} : wt v = ‖v‖₀

theorem Code.wt_eq_zero_iff {F : Type u_3} [DecidableEq F] {ι : Type u_4} [Fintype ι] [Zero F] {v : ι → F} : wt v = 0 ↔ Fintype.card ι = 0 ∨ ∀ (i : ι), v i = 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

@[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.fromRowGenMat {F : Type u_3} {ι : Type u_4} [Fintype ι] {κ : Type u_5} [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

noncomputable def LinearCode.fromColGenMat {F : Type u_3} {ι : Type u_4} [Fintype ι] {κ : Type u_5} [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.byCheckMatrix {F : Type u_3} {ι : Type u_4} {κ : Type u_5} [Fintype κ] [CommRing F] (H : Matrix ι κ F) : LinearCode κ F

Define a linear code from its (parity) check matrix

Equations

• LinearCode.byCheckMatrix H = LinearMap.ker H.mulVecLin

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

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

• LC.disFromHammingNorm = sInf {d : ℕ | ∃ u ∈ LC, u ≠ 0 ∧ ‖u‖₀ ≤ d}

theorem LinearCode.dist_eq_dist_from_HammingNorm {F : Type u_3} {ι : Type u_4} [Fintype ι] [Semiring F] [DecidableEq F] (LC : LinearCode ι F) : ‖LC.carrier‖₀ = LC.disFromHammingNorm

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

The dimension of a linear code.

Equations

• LC.dim = Module.finrank F ↥LC

theorem LinearCode.rank_eq_dim_fromColGenMat {F : Type u_3} {ι : Type u_4} [Fintype ι] {κ : Type u_5} [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_4} [Fintype ι] [Semiring F] : LinearCode ι F → ℕ

The length of a linear code.

Equations

• x✝.length = Fintype.card ι

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

The rate of a linear code.

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} [DecidableEq F] {ι : Type u_4} [Fintype ι] [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 ∧ Code.wt c = w}

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

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

theorem LinearCode.dist_eq_minWtCodewords {F : Type u_3} [DecidableEq F] {ι : Type u_4} [Fintype ι] [CommRing F] {LC : LinearCode ι F} : Code.minDist ↑LC = LC.minWtCodewords

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

theorem LinearCode.dist_UB {F : Type u_3} [DecidableEq F] {ι : Type u_4} [Fintype ι] [CommRing F] {LC : LinearCode ι F} : Code.minDist ↑LC ≤ LC.length

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

def LinearCode.interleaveCode {n : Type u_1} {F : Type u_3} [Semiring F] [DecidableEq F] (C : Submodule F (n → F)) (ι : Type u_5) : Submodule F (ι × n → F)

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

Equations

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

def LinearCode.«term_^⋈_» : Lean.TrailingParserDescr

Equations

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

def LinearCode.Function.interleave₂ {α : Type u_5} {β : Type u_6} (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 LinearCode.«term_⋈_» : Lean.TrailingParserDescr

Equations

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

theorem LinearCode.singleton_bound_linear {n : Type u_1} [Fintype n] {F : Type u_3} [DecidableEq F] {ι : Type u_4} [Fintype ι] [Semiring F] (LC : LinearCode ι F) : Module.finrank F ↥LC ≤ Fintype.card n - ‖LC.carrier‖₀ + 1

Singleton bound for linear codes

def LinearCode.linearCodeDist' {F : Type u_3} {ι : Type u_4} [Fintype ι] [Semiring F] [DecidableEq F] [Fintype F] [DecidableEq ι] (LC : LinearCode ι F) [DecidablePred fun (x : ι → F) => x ∈ LC] : ℕ∞

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

Equations

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

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