Helper

dotp_n_e1

Section malicious_n

Type Lemma

Proof Lines 7

Lemma dotp_n_e1 (v : {ffun 'I_n_relay.+1 -> msg}) : dotp_n ConstUS_n v = v ord0.

e_1 . v = v_1: the first basis vector extracts the first component

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

No lemmas in the stats use this lemma.

Loading source code...