Diffusion afp-devel 588a85942e31

new entry: Smith normal form
588a85942e31
Actions

Tags

None

Subscribers

None

Description

new entry: Smith normal form

Details

Provenance

Rene Thiemann <rene.thiemann@uibk.ac.at>

Authored on

Parents

rAFPe90b3aeb001d: changed import to prepare for Smith-Normal-Form submission

Branches

Unknown

Tags

Unknown

Event Timeline

Rene Thiemann <rene.thiemann@uibk.ac.at> committed rAFP588a85942e31: new entry: Smith normal form.May 25 2020, 2:32 PM

Changes (26)

Path

Size

Smith_Normal_Form

Admits_SNF_From_Diagonal_Iff_Bezout_Ring.thy

Cauchy_Binet.thy

Cauchy_Binet_HOL_Analysis.thy

Diagonal_To_Smith.thy

Diagonal_To_Smith_JNF.thy

Diagonalize.thy

Elementary_Divisor_Rings.thy

Finite_Field_Mod_Type_Connection.thy

Mod_Type_Connect.thy

Rings2_Extended.thy

SNF_Algorithm.thy

SNF_Algorithm_Euclidean_Domain.thy

SNF_Algorithm_HOL_Analysis.thy

SNF_Algorithm_Two_Steps.thy

SNF_Algorithm_Two_Steps_JNF.thy

SNF_Missing_Lemmas.thy

SNF_Uniqueness.thy

Smith_Certified.thy

Smith_Normal_Form.thy

Smith_Normal_Form_JNF.thy

rAFP588a85942e31

thys/ROOTS

Loading...

thys/Smith_Normal_Form/Admits_SNF_From_Diagonal_Iff_Bezout_Ring.thy

Loading...

thys/Smith_Normal_Form/Cauchy_Binet.thy

Loading...

thys/Smith_Normal_Form/Cauchy_Binet_HOL_Analysis.thy

Loading...

thys/Smith_Normal_Form/Diagonal_To_Smith.thy

Loading...

thys/Smith_Normal_Form/Diagonal_To_Smith_JNF.thy

Loading...

thys/Smith_Normal_Form/Diagonalize.thy

Loading...

thys/Smith_Normal_Form/Elementary_Divisor_Rings.thy

Loading...

thys/Smith_Normal_Form/Finite_Field_Mod_Type_Connection.thy

Loading...

thys/Smith_Normal_Form/Mod_Type_Connect.thy

Loading...

thys/Smith_Normal_Form/ROOT

Loading...

thys/Smith_Normal_Form/Rings2_Extended.thy

Loading...

thys/Smith_Normal_Form/SNF_Algorithm.thy

Loading...

thys/Smith_Normal_Form/SNF_Algorithm_Euclidean_Domain.thy

Loading...

thys/Smith_Normal_Form/SNF_Algorithm_HOL_Analysis.thy

Loading...

thys/Smith_Normal_Form/SNF_Algorithm_Two_Steps.thy

Loading...

thys/Smith_Normal_Form/SNF_Algorithm_Two_Steps_JNF.thy

Loading...

thys/Smith_Normal_Form/SNF_Missing_Lemmas.thy

Loading...

thys/Smith_Normal_Form/SNF_Uniqueness.thy

Loading...

thys/Smith_Normal_Form/Smith_Certified.thy

Loading...

thys/Smith_Normal_Form/Smith_Normal_Form.thy

Loading...

thys/Smith_Normal_Form/Smith_Normal_Form_JNF.thy

Loading...

thys/Smith_Normal_Form/document/root.tex

Loading...