Smith_Normal_Form

Diagonal_To_Smith

Mod_Type_Connect

SNF_Missing_Lemmas

Cauchy_Binet

Smith_Normal_Form_JNF

Rings2_Extended

Finite_Field_Mod_Type_Connection

Admits_SNF_From_Diagonal_Iff_Bezout_Ring

SNF_Uniqueness

Cauchy_Binet_HOL_Analysis

Diagonalize

SNF_Algorithm_Two_Steps

Diagonal_To_Smith_JNF

SNF_Algorithm_Two_Steps_JNF

SNF_Algorithm

SNF_Algorithm_HOL_Analysis

Elementary_Divisor_Rings

SNF_Algorithm_Euclidean_Domain

Smith_Certified

Alternative_Proofs