Main

count_affine_solutions_explicit_col

File dumas2017dual/lib/rouche_capelli.v

Section affine_solultion_counting_col

Type Lemma

Proof Lines 6

Signature

Lemma count_affine_solutions_explicit_col (v0 : 'cV[K]_n) : A *m v0 = b -> #|affine_solutions_col| = (#|{:K}| ^ (n - \rank A))%N.

Description

Explicit affine count (column version): |{v | Av = b}| = |K|^(n - rank(A)). Main Rouché-Capelli formula for Av = b systems. Used in DSDP fiber counting where constraints are expressed as column multiplication.

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