Helper

constraint_proj

File dumas2017dual/entropy_fiber/linear_fiber_zpq.v

Section fiber_2d

Type Lemma

Proof Lines 5

Signature

Lemma constraint_proj (u2 u3 target : msg) (vv : msg * msg) : u2 * vv.1 + u3 * vv.2 = target -> (proj_Fp u2 * proj_Fp vv.1 + proj_Fp u3 * proj_Fp vv.2 = proj_Fp target) /\ (proj_Fq u2 * proj_Fq vv.1 + proj_Fq u3 * proj_Fq vv.2 = proj_Fq target).

Description

Constraint correspondence between Z_m and field components

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