Helper

limg_lker

Section vector_ext

Type Lemma

Proof Lines 1

Lemma limg_lker {K : fieldType} {aT rT : vectType K} (f : 'Hom(aT, rT)) : (f @: lker f = 0)%VS.

Image of kernel is zero: f(ker(f)) = 0. By definition of kernel.

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

No lemmas in the stats use this lemma.

Loading source code...