Helper

card_lker_Hom

Section counting

Type Lemma

Proof Lines 8

Lemma card_lker_Hom : #|lker (Hom A)| = #|[set x : 'rV[K]_m | x *m A == 0]|.

Kernel cardinality for Hom functor: |ker(Hom(A))| = |{x | xA = 0}|. Specializes card_lker_mxof to the standard matrix-to-linear-map coercion.

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

No lemmas in the stats use this lemma.

Loading source code...