fact: Fixpoint smithmxn_rec m n : 'M[R]_(1 + (1 + m),1 + (1 + n)) -> 'M[R]_(1 + (1 + m)) * seq R * 'M[R]_(1 + (1 + n)) := match m,n with | 0,_ => fun A => smith2xn A | _,0 => fun A => let: (L,d,R) := smith2xn A^T in (R^T,d,L^T) | m'.+1,n'.+1 => fun A => let: A1 := usubmx A in let: A2 := dsubmx A in let: (P1,x,Q1) := smithmxn_rec A2 in let: C := col_mx (A1 *m Q1) (P1 *m A2 *m Q1) in let: D := col_mx (row 0 C) (row 1 C) in let: E := dsubmx (dsubmx C) in let: (P2,y,Q2) := smith2xn D in let: H := col_mx (P2 *m D *m Q2) (E *m Q2) : 'M[R]_(1 + _, 1 + _) in let: y := y`_0 in let: c' := map_mx (fun x => odflt 0 (x %/? y)) (dlsubmx H) in let: (L1,d,R1) := smithmxn_rec (drsubmx H) in let: P := block_mx P2 0 0 1%:M : 'M[R]_(1 + _) in (block_mx 1%:M 0 (- L1 *m c') L1 *m P *m lift0_mx P1, y :: d, Q1 *m Q2 *m lift0_mx R1) end.
imports: HB(structures) mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat div seq path) mathcomp(ssralg fintype matrix mxalgebra bigop zmodp perm choice) dvdring mxstructure minor stronglydiscrete coherent edr