Helper

HomK

Section vector_ext

Type Lemma

Proof Lines 1

Lemma HomK {R : nzRingType} {vT wT : vectType R} (A : 'M_(dim vT, dim wT)) : f2mx (Hom A) = A.

Matrix representation of Hom: f2mx(Hom(A)) = A. Coercion identity.

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

No lemmas in the stats use this lemma.

Loading source code...