Helper

idealized_Epow_scalarM

File homomorphic_encryption/idealized/idealized_ahe.v

Section Idealized_AHE

Type Lemma

Proof Lines 5

Signature

Lemma idealized_Epow_scalarM : forall (k : pub_key IT) (j : plain IT), {morph enc_curry IT k : mr / mr_bop_rplain IT *%R idealized_rand_pow mr j >-> idealized_Epow mr j}.

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