fact: Fixpoint smith2xn n : 'M[R]_(2,1 + (1 + n)) -> 'M[R]_2 * seq R * 'M[R]_n.+2 := if n is p.+1 then fun A : 'M[R]_(2,1 + _) => let: A1 := lsubmx A in let: A2 := rsubmx A in let: (P1,d1,Q1) := smith2xn A2 in let: C := row_mx (P1 *m A1) (P1 *m A2 *m Q1) : 'M[R]_(2,1 + (1 + _)) in let: D := row_mx (col 0 C) (col 1 C) in let: E := rsubmx (rsubmx C) in let: (P2,d2,Q2) := smith2x2 D in let: H := row_mx (P2 *m D *m Q2) (P2 *m E) : 'M[R]_(1 + 1, 1 + _) in let: y := d2`_0 in let: r' := map_mx (fun x => odflt 0 (x %/? y)) (ursubmx H) in let: H' := drsubmx H : 'rV_(2 + _) in let: (L1,d,R1) := smith1xn smith2x2 (lsubmx H') in let: R1' := (block_mx R1 0 0 1%:M) in (lift0_mx L1 *m P2 *m P1, y :: d, lift0_mx Q1 *m block_mx Q2 0 0 1%:M *m block_mx 1%:M (- r' *m R1') 0 R1') else fun A => smith2x2 A.
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