search

affeldt-aist / infotheo

A Coq formalization of information theory and linear error-correcting codes
GNU Lesser General Public License v2.1
64 stars 15 forks source link

Merge scaled convex #2

Closed garrigue closed 5 years ago

garrigue commented 5 years ago

I also removed all the extra code that was used to prove Convn_perm. But I may have removed too much...