Session Stochastic_Matrices
View
theory dependencies
View
document
View
outline
Theories
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
HOL-Library.More_List
HOL-Computational_Algebra.Polynomial
HOL-Computational_Algebra.Fraction_Field
HOL-Computational_Algebra.Normalized_Fraction
HOL-Computational_Algebra.Polynomial_Factorial
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.Matrix_Kernel
Jordan_Normal_Form.Jordan_Normal_Form_Uniqueness
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
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›
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
Perron_Frobenius.Perron_Frobenius_Aux
Perron_Frobenius.Perron_Frobenius
Perron_Frobenius.Roots_Unity
Rank_Nullity_Theorem.Dual_Order
Rank_Nullity_Theorem.Mod_Type
HOL-Library.Function_Algebras
Rank_Nullity_Theorem.Miscellaneous
Perron_Frobenius.Perron_Frobenius_Irreducible
Stochastic_Matrix
Stochastic_Vector_PMF
Stochastic_Matrix_Markov_Models
Eigenspace
Stochastic_Matrix_Perron_Frobenius