Helper

card_translate

Section affine_solution_counting

Type Lemma

Proof Lines 5

Lemma card_translate (S : {set 'rV[K]_m}) (v : 'rV[K]_m) : #|[set v + s | s in S]| = #|S|.

Translation preserves cardinality: |v + S| = |S|. Adding a constant vector v to all elements is a bijection.

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

No lemmas in the stats use this lemma.

Loading source code...