proposition: Lemma det_Smith n (M: 'M[E]_n) : \det (Smith_form M) = \det M.
proof: Proof. rewrite /Smith_form /Smith_seq. case: n M=>[M|n M]; first by rewrite !det_mx00. case: (SmithP find1P find2P find_pivotP)=> L0 d R0 H _ HL0 HR0. case: d H=>[|a l]. rewrite !diag_mx_seq_nil -{1}(mul0mx _ R0)=> /(mulIr HR0). by rewrite -{1}(mulmx0 _ L0)=> /(mulrI HL0)=> ->. rewrite !diag_mx_seq_cons (@det_ublock _ 1) scalar_mxM detM -mulrA. rewrite -(det_ublock a%:M 0)=> <-. rewrite !detM -invrM -?unitmxE // det_scalar1 (mulrC (\det L0)). rewrite -mulrA mulrC -(mulrA (\det M)) (mulrC (\det L0)) mulrV ?mulr1 //. by rewrite unitrM -!unitmxE HR0. Qed.
imports: mathcomp(all_ssreflect) mathcomp(all_algebra) mathcomp(all_fingroup) mathcomp(all_real_closed) CoqEAL(binetcauchy ssrcomplements mxstructure minor) CoqEAL(smith dvdring polydvd) CoqEAL(similar perm_eq_image)