Helper

crt_proj_pair_fiber

File dumas2017dual/entropy_fiber/linear_fiber_zpq.v

Section fiber_2d

Type Lemma

Proof Lines 6

Signature

Lemma crt_proj_pair_fiber (u2 u3 target : msg) (vv : msg * msg) : vv \in linear_fiber_2d u2 u3 target -> crt_proj_pair vv \in setX (fiber_Fp (proj_Fp u2) (proj_Fp u3) (proj_Fp target)) (fiber_Fq (proj_Fq u2) (proj_Fq u3) (proj_Fq 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