proposition: Lemma limg_ker_dim f U : (\dim (U :&: lker f) + \dim (f @: U) = \dim U)%N.
proof: Proof. rewrite unlock /dimv /= genmx_cap genmx_id -genmx_cap !genmxE. by rewrite addnC mxrank_mul_ker. Qed.
imports: HB(structures) mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat seq choice) mathcomp(fintype bigop finfun tuple) mathcomp(ssralg matrix mxalgebra zmodp)