Session Smith_Normal_Form
View
theory dependencies
View
document
View
outline
Theories
HOL-Types_To_Sets.Types_To_Sets
File ‹local_typedef.ML›
File ‹unoverloading.ML›
File ‹internalize_sort.ML›
File ‹unoverload_type.ML›
File ‹unoverload_def.ML›
Smith_Normal_Form
Diagonal_To_Smith
Polynomial_Interpolation.Ring_Hom
Jordan_Normal_Form.Missing_Misc
HOL-Algebra.Congruence
HOL-Algebra.Order
HOL-Algebra.Lattice
HOL-Algebra.Complete_Lattice
HOL-Algebra.Group
HOL-Algebra.FiniteProduct
HOL-Algebra.Ring
File ‹ringsimp.ML›
Jordan_Normal_Form.Missing_Ring
Jordan_Normal_Form.Conjugate
HOL-Algebra.Module
Jordan_Normal_Form.Matrix
Polynomial_Interpolation.Missing_Unsorted
Polynomial_Interpolation.Missing_Polynomial
Polynomial_Factorization.Order_Polynomial
HOL-Computational_Algebra.Fundamental_Theorem_Algebra
Polynomial_Factorization.Fundamental_Theorem_Algebra_Factorized
Polynomial_Interpolation.Ring_Hom_Poly
Jordan_Normal_Form.Gauss_Jordan_Elimination
Jordan_Normal_Form.Column_Operations
Jordan_Normal_Form.Determinant
Jordan_Normal_Form.Char_Poly
Jordan_Normal_Form.Jordan_Normal_Form
HOL-Algebra.Coset
VectorSpace.RingModuleFacts
VectorSpace.FunctionLemmas
VectorSpace.MonoidSums
VectorSpace.LinearCombinations
VectorSpace.SumSpaces
VectorSpace.VectorSpace
Jordan_Normal_Form.Missing_VectorSpace
Jordan_Normal_Form.VS_Connect
Jordan_Normal_Form.Gram_Schmidt
Jordan_Normal_Form.Schur_Decomposition
Jordan_Normal_Form.Jordan_Normal_Form_Existence
Jordan_Normal_Form.Spectral_Radius
Perron_Frobenius.Bij_Nat
Perron_Frobenius.Cancel_Card_Constraint
File ‹cancel_card_constraint.ML›
HOL-Eisbach.Eisbach
File ‹parse_tools.ML›
File ‹method_closure.ML›
File ‹eisbach_rule_insts.ML›
File ‹match_method.ML›
Perron_Frobenius.HMA_Connect
Mod_Type_Connect
Jordan_Normal_Form.DL_Missing_List
Jordan_Normal_Form.DL_Rank
Jordan_Normal_Form.DL_Missing_Sublist
Jordan_Normal_Form.DL_Submatrix
Jordan_Normal_Form.DL_Rank_Submatrix
List-Index.List_Index
SNF_Missing_Lemmas
Cauchy_Binet
Smith_Normal_Form_JNF
Rings2_Extended
HOL-Number_Theory.Cong
HOL-Algebra.AbelCoset
HOL-Algebra.Ideal
HOL-Algebra.RingHom
HOL-Algebra.UnivPoly
HOL-Algebra.Generated_Groups
HOL-Algebra.Elementary_Groups
HOL-Algebra.Multiplicative_Group
HOL-Number_Theory.Totient
HOL-Number_Theory.Residues
Subresultants.Binary_Exponentiation
Berlekamp_Zassenhaus.Finite_Field
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
Deriving.Generator_Aux
File ‹bnf_access.ML›
File ‹generator_aux.ML›
Deriving.Derive_Manager
File ‹derive_manager.ML›
Show.Show
File ‹show_generator.ML›
Show.Show_Instances
Jordan_Normal_Form.Show_Matrix
Show.Show_Poly
SNF_Algorithm_Euclidean_Domain
Smith_Certified
Alternative_Proofs