mathlib4 icon indicating copy to clipboard operation
mathlib4 copied to clipboard

Published 20 hours ago • verified publisher icon leanprover-community

feat: Berlekamp-Welch

Open BoltonBailey opened this issue 1 year ago • 0 comments

Implementation of the Berlekamp-Welch Decoding procedure, and proof of its correctness within the decoding radius.

Todos:

  • [ ] Integrate with coding theory part of library
  • [ ] Gaussian Elimination lives in Mathlib/Tactic/Linarith/SimplexAlgorithm/Gauss.lean, may need facts about it.

Open in Gitpod

BoltonBailey avatar Apr 13 '24 01:04 BoltonBailey