proposition: Lemma mxrank_mul_ker m n p (A : 'M_(m, n)) (B : 'M_(n, p)) : (\rank (A *m B) + \rank (A :&: kermx B))%N = \rank A.
proof: Proof. apply/eqP; set K := kermx B; set C := (A :&: K)%MS. rewrite -(eqmxMr B (eq_row_base A)); set K' := _ *m B. rewrite -{2}(subnKC (rank_leq_row K')) -mxrank_ker eqn_add2l. rewrite -(mxrankMfree _ (row_base_free A)) mxrank_leqif_sup. by rewrite sub_capmx -(eq_row_base A) submxMl sub_kermx -mulmxA mulmx_ker/=. have /submxP[C' defC]: (C <= row_base A)%MS by rewrite eq_row_base capmxSl. by rewrite defC submxMr // sub_kermx mulmxA -defC -sub_kermx capmxSr. Qed.
imports: HB(structures) mathcomp(ssreflect ssrbool ssrfun eqtype ssrnat seq choice) mathcomp(fintype finfun bigop finset fingroup perm order) mathcomp(div prime binomial ssralg finalg zmodp matrix)