Helper

count_kernel_vectors_col

File dumas2017dual/lib/rouche_capelli.v

Section affine_solultion_counting_col

Type Lemma

Proof Lines 16

Signature

Lemma count_kernel_vectors_col : #|[set v : 'cV[K]_n | A *m v == 0]| = (#|{:K}| ^ (n - \rank A))%N.

Description

Kernel cardinality (column version): |{v | Av = 0}| = |K|^(n - rank(A)). Proved by transposing to row form and applying count_kernel_vectors. Needed because Coq treats 'cV and 'rV as distinct types.

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