proposition: Lemma mulmx_max_rank r m n (M : 'M_(m, r)) (N : 'M_(r, n)) : \rank (M *m N) <= r.
proof: Proof. set MN := M *m N; set rMN := \rank _. pose L : 'M_(rMN, m) := pid_mx rMN *m invmx (col_ebase MN). pose U : 'M_(n, rMN) := invmx (row_ebase MN) *m pid_mx rMN. suffices: L *m M *m (N *m U) = 1%:M by apply: mulmx1_min. rewrite mulmxA -(mulmxA L) -[M *m N]mulmx_ebase -/MN. by rewrite !mulmxA mulmxKV // mulmxK // !pid_mx_id /rMN ?pid_mx_1. 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)