Helper

constraint_crt

File dumas2017dual/entropy_fiber/linear_fiber_zpq.v

Section fiber_2d

Type Lemma

Proof Lines 11

Signature

Lemma constraint_crt (u2 u3 target : msg) (pp : 'F_p * 'F_p) (qq : 'F_q * 'F_q) : proj_Fp u2 * pp.1 + proj_Fp u3 * pp.2 = proj_Fp target -> proj_Fq u2 * qq.1 + proj_Fq u3 * qq.2 = proj_Fq target -> u2 * (crt_pair pp qq).1 + u3 * (crt_pair pp qq).2 = target.

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