mathlib3

feat(information_theory/linear_code): Define linear codes

#16774

Open