Helper

count_kernel_vectors

File dumas2017dual/lib/rouche_capelli.v

Section counting

Type Lemma

Proof Lines 3

Signature

Lemma count_kernel_vectors : #| [set x : 'rV[K]_m | x *m A == 0] | = (#| {:K} | ^ (m - \rank A))%N.

Description

Kernel cardinality formula: |ker(A)| = |K|^(m - rank(A)). The kernel is a subspace of dimension (m - rank(A)), hence has this many elements. This is the core counting result for linear systems.

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