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

generalize and cleanup some lemmas for bigop #108

Closed t6s closed 10 months ago

t6s commented 10 months ago

This PR generalizes some lemma on bigop from reals to more abstract algebras. Some cleanups on the proofs are also done.

No harm on the wrt_infotheo_master branch of monae.