Helper

entropy_formula_same

File dumas2017dual/lib/extra_algebra.v

Section Zp_Fp_equivalence

Type Lemma

Proof Lines 1

Signature

Lemma entropy_formula_same (m : nat) : (1 < m)%N -> log (m%:R : R) = log (m%:R : R).

Description

Reflexivity lemma for entropy formulas over Z_m. This trivial lemma serves as a proof obligation discharge when showing that entropy calculations over different representations (e.g., 'Z_m vs 'F_m when m is prime) yield identical results.

Uses (0)

This lemma does not use any other lemmas from the stats.

Used By (0)

No lemmas in the stats use this lemma.

Coq Source Code

View on GitHub

Loading source code...

← Back to Stats