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

interface consistency #24

Closed affeldt-aist closed 3 years ago

affeldt-aist commented 3 years ago

mulRV : forall x : R, x != 0 -> x / x = 1 invRM : forall r1 r2 : R, r1 <> 0 -> r2 <> 0 -> / (r1 r2) = / r1 * / r2

@t6s