Changes

Summary

documented new development in Perron Frobenius
cleanup in theories by moving lemmas to proper places

Changeset 8496:6e32bf48ba30 by rene thiemann _rene.thiemann@uibk.ac.at_: documented new development in Perron Frobenius
The file was modified	`metadata/metadata` (diff)
Changeset 8495:07ea45e2d48b by rene thiemann _rene.thiemann@uibk.ac.at_: cleanup in theories by moving lemmas to proper places
The file was modified	`thys/Jordan_Normal_Form/Char_Poly.thy` (diff)
The file was modified	`thys/Jordan_Normal_Form/Determinant.thy` (diff)
The file was modified	`thys/Jordan_Normal_Form/Jordan_Normal_Form.thy` (diff)
The file was modified	`thys/Jordan_Normal_Form/Jordan_Normal_Form_Existence.thy` (diff)
The file was modified	`thys/Jordan_Normal_Form/Matrix.thy` (diff)
The file was modified	`thys/Perron_Frobenius/HMA_Connect.thy` (diff)
The file was modified	`thys/Perron_Frobenius/Perron_Frobenius.thy` (diff)
The file was modified	`thys/Perron_Frobenius/Perron_Frobenius_Aux.thy` (diff)
The file was modified	`thys/Perron_Frobenius/Perron_Frobenius_Irreducible.thy` (diff)
The file was modified	`thys/Perron_Frobenius/Roots_Unity.thy` (diff)
The file was modified	`thys/Perron_Frobenius/Spectral_Radius_Theory.thy` (diff)
The file was modified	`thys/Polynomial_Factorization/Order_Polynomial.thy` (diff)
The file was modified	`thys/Polynomial_Factorization/ROOT` (diff)
The file was modified	`thys/Polynomial_Interpolation/Missing_Polynomial.thy` (diff)
The file was modified	`thys/Polynomial_Interpolation/Ring_Hom.thy` (diff)
The file was modified	`thys/Polynomial_Interpolation/Ring_Hom_Poly.thy` (diff)
The file was removed	`thys/Perron_Frobenius/Perron_Frobenius_Aux_2.thy`