Session Jordan_Normal_Form

Theories

• Missing_Misc
• Missing_Ring
• Polynomial_Interpolation.Ring_Hom
• Conjugate
• Matrix
• Containers.Containers_Auxiliary
• Deriving.Generator_Aux
  • File ‹bnf_access.ML›
  • File ‹generator_aux.ML›
• Deriving.Derive_Manager
  • File ‹derive_manager.ML›
• Containers.Containers_Generator
  • File ‹containers_generator.ML›
• Containers.Collection_Enum
  • File ‹cenum_generator.ML›
• Deriving.Equality_Generator
  • File ‹equality_generator.ML›
• Deriving.Equality_Instances
• Containers.Collection_Eq
  • File ‹ceq_generator.ML›
• Containers.Equal
• Containers.DList_Set
• Containers.List_Fusion
• Containers.Lexicographic_Order
• Containers.Extend_Partial_Order
• Containers.Set_Linorder
• Deriving.Comparator
• Deriving.Comparator_Generator
  • File ‹comparator_generator.ML›
• Deriving.Compare
  • File ‹compare_code.ML›
• Deriving.Compare_Generator
  • File ‹compare_generator.ML›
• Deriving.Compare_Instances
• Containers.Collection_Order
  • File ‹ccompare_generator.ML›
• Containers.RBT_ext
• Deriving.RBT_Comparator_Impl
• Containers.RBT_Mapping2
• Containers.RBT_Set2
• Containers.Closure_Set
• Containers.Set_Impl
  • File ‹set_impl_generator.ML›
• Matrix_IArray_Impl
• Polynomial_Interpolation.Missing_Unsorted
• Gauss_Jordan_Elimination
• Gauss_Jordan_IArray_Impl
• Polynomial_Interpolation.Missing_Polynomial
• Column_Operations
• Determinant
• Determinant_Impl
• Show.Show
  • File ‹show_generator.ML›
• Show_Matrix
• Show.Show_Instances
• Show.Shows_Literal
• Shows_Literal_Matrix
• Polynomial_Factorization.Order_Polynomial
• Polynomial_Factorization.Fundamental_Theorem_Algebra_Factorized
• Polynomial_Interpolation.Ring_Hom_Poly
• Char_Poly
• Jordan_Normal_Form
• VectorSpace.RingModuleFacts
• VectorSpace.FunctionLemmas
• VectorSpace.MonoidSums
• VectorSpace.LinearCombinations
• VectorSpace.SumSpaces
• VectorSpace.VectorSpace
• Missing_VectorSpace
• VS_Connect
• Gram_Schmidt
• Schur_Decomposition
• Jordan_Normal_Form_Existence
• Matrix_Impl
• Strassen_Algorithm
• Strassen_Algorithm_Code
• Regular-Sets.Regular_Set
• Regular-Sets.Regular_Exp
• Regular-Sets.NDerivative
• Regular-Sets.Equivalence_Checking
• Regular-Sets.Relation_Interpretation
• Regular-Sets.Regexp_Method
• Abstract-Rewriting.Seq
• Abstract-Rewriting.Abstract_Rewriting
• Abstract-Rewriting.SN_Orders
• Matrix.Ordered_Semiring
• Matrix_Comparison
• Abstract-Rewriting.SN_Order_Carrier
• Ring_Hom_Matrix
• Derivation_Bound
• Complexity_Carrier
• Show_Arctic
• Matrix_Complexity
• Matrix_Kernel
• Jordan_Normal_Form_Uniqueness
• Spectral_Radius
• DL_Missing_List
• DL_Rank
• DL_Missing_Sublist
• DL_Submatrix
• DL_Rank_Submatrix