Helper

count_affine_solutions

Section affine_solution_counting

Type Lemma

Proof Lines 5

Lemma count_affine_solutions (x0 : 'rV[K]_m) : x0 *m A = b -> #|affine_solutions| = #|kernel_solutions|.

Affine solutions = kernel cardinality: |{x | xA = b}| = |ker(A)|. Since affine_solutions = x₀ + ker(A), cardinality equals kernel size.

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

No lemmas in the stats use this lemma.

Loading source code...