Helper

crt_pair_fiber

File dumas2017dual/entropy_fiber/linear_fiber_zpq.v

Section fiber_2d

Type Lemma

Proof Lines 3

Signature

Lemma crt_pair_fiber (u2 u3 target : msg) (pp : 'F_p * 'F_p) (qq : 'F_q * 'F_q) : pp \in fiber_Fp (proj_Fp u2) (proj_Fp u3) (proj_Fp target) -> qq \in fiber_Fq (proj_Fq u2) (proj_Fq u3) (proj_Fq target) -> crt_pair pp qq \in linear_fiber_2d u2 u3 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