Linear codes

A linear code is a submodule C of the words ι → M, usually with M = F a field MacWilliams and Sloane, Chapter 1. The Hamming distance between two words is the Hamming weight hammingNorm of their difference, and the difference of two codewords is a codeword, so the minimum distance of a linear code is the least weight of a nonzero codeword (Cslib.Code.le_minDist_iff_hammingNorm, Cslib.Code.minDist_eq_iInf_hammingNorm).

Main results

• Cslib.Code.le_minDist_iff_hammingNorm: lower bounds on the minimum distance of a linear code are lower bounds on the weights of its nonzero codewords.
• Cslib.Code.minDist_eq_iInf_hammingNorm: the minimum distance of a linear code is the least weight of a nonzero codeword.

References

• [F. J. MacWilliams, N. J. A. Sloane, The Theory of Error-Correcting Codes] [MWS77]

theorem Cslib.Code.le_minDist_iff_hammingNorm {ι : Type u_1} {R : Type u_2} {M : Type u_3} [Fintype ι] [Ring R] [AddCommGroup M] [Module R M] [DecidableEq M] (C : Submodule R (ι → M)) {d : ℕ∞} : d ≤ minDist ↑C ↔ ∀ x ∈ C, x ≠ 0 → d ≤ ↑(hammingNorm x)

The minimum distance of a linear code is at least d iff every nonzero codeword has weight at least d.

theorem Cslib.Code.minDist_eq_iInf_hammingNorm {ι : Type u_1} {R : Type u_2} {M : Type u_3} [Fintype ι] [Ring R] [AddCommGroup M] [Module R M] [DecidableEq M] (C : Submodule R (ι → M)) : minDist ↑C = ⨅ x ∈ C, ⨅ (_ : x ≠ 0), ↑(hammingNorm x)

Minimum weight. The minimum distance of a linear code is the least weight of a nonzero codeword, and ⊤ for the zero code.