Helper

card_translate_col

Section affine_solultion_counting_col

Type Lemma

Proof Lines 5

Lemma card_translate_col (S : {set 'cV[K]_n}) (v : 'cV[K]_n) : #|[set v + s | s in S]| = #|S|.

Translation preserves cardinality (column version): |v + S| = |S|. Same as card_translate but for column vectors.

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

No lemmas in the stats use this lemma.

Loading source code...