feat(information_theory/linear_code): Define linear codes

[BoltonBailey]

Add linear codes and defines the Reed-Solomon code.

• [ ] depends on: #15689

---

[linesthatinterlace]

I feel a bit stupid because I've written versions of this same file a bunch of times in the last few months, I never submitted it, and now you actually did it - well done. However: my suspicion is that you might run into the same issues I did.

What this file lacks is many or any theorems. You're doing a lot of defining things - but every definition comes with a cost. What I want to see is some theorems proving (not necessarily complicated!) facts about these objects.

In addition - it doesn't make sense to me to define linear codes without first defining block codes, which was a sticking point for me. You're not really using the linearity that much in what you've done so far.

I would expect to see some mention of generating matrices and parity check matrices...

[linesthatinterlace]

I would be interested to see if you could base this off my infsep branch. That construction was intended for use in a PR like this - it was held up for a month by some PR issues.

[mathlib-dependent-issues-bot]

This PR/issue depends on:

• ~~leanprover-community/mathlib#15689~~ By Dependent Issues (🤖). Happy coding!