Changes

Summary

merge
moved several lemmas (consolidate Missing_... with main theories)
merge
reuse generalized theorems in Factor_Bound_2 in Mahler_Measure and Factor_Bound

Changeset 8883:264d56ddacaf by rene thiemann _rene.thiemann@uibk.ac.at_: merge
Changeset 8882:89ba3226904a by rene thiemann _rene.thiemann@uibk.ac.at_: moved several lemmas (consolidate Missing_... with main theories)
The file was modified	`thys/Algebraic_Numbers/Complex_Roots_Real_Poly.thy` (diff)
The file was modified	`thys/Berlekamp_Zassenhaus/Berlekamp_Type_Based.thy` (diff)
The file was modified	`thys/Berlekamp_Zassenhaus/Matrix_Record_Based.thy` (diff)
The file was modified	`thys/Deep_Learning/DL_Concrete_Matrices.thy` (diff)
The file was modified	`thys/Deep_Learning/DL_Deep_Model.thy` (diff)
The file was modified	`thys/Deep_Learning/DL_Network.thy` (diff)
The file was modified	`thys/Deep_Learning/DL_Rank_CP_Rank.thy` (diff)
The file was modified	`thys/Jordan_Normal_Form/Conjugate.thy` (diff)
The file was modified	`thys/Jordan_Normal_Form/DL_Rank.thy` (diff)
The file was modified	`thys/Jordan_Normal_Form/DL_Rank_Submatrix.thy` (diff)
The file was modified	`thys/Jordan_Normal_Form/Determinant.thy` (diff)
The file was modified	`thys/Jordan_Normal_Form/Matrix.thy` (diff)
The file was modified	`thys/Jordan_Normal_Form/Missing_VectorSpace.thy` (diff)
The file was modified	`thys/Jordan_Normal_Form/VS_Connect.thy` (diff)
The file was modified	`thys/LLL_Basis_Reduction/Missing_Lemmas.thy` (diff)
The file was modified	`thys/LLL_Basis_Reduction/ROOT` (diff)
The file was modified	`thys/Polynomial_Factorization/Missing_Polynomial_Factorial.thy` (diff)
The file was modified	`thys/Polynomial_Interpolation/Missing_Polynomial.thy` (diff)
The file was modified	`thys/Polynomial_Interpolation/Missing_Unsorted.thy` (diff)
The file was modified	`thys/Sqrt_Babylonian/Sqrt_Babylonian.thy` (diff)
The file was removed	`thys/Jordan_Normal_Form/DL_Missing_Matrix.thy`
The file was removed	`thys/Jordan_Normal_Form/DL_Missing_VS_Connect.thy`
The file was removed	`thys/Jordan_Normal_Form/DL_Missing_Vector_Space.thy`
The file was removed	`thys/LLL_Basis_Reduction/Vector_Lattice_Locale.thy`
Changeset 8881:a648554bb187 by rene thiemann _rene.thiemann@uibk.ac.at_: merge
Changeset 8880:15646aa87593 by rene thiemann _rene.thiemann@uibk.ac.at_: reuse generalized theorems in Factor_Bound_2 in Mahler_Measure and Factor_Bound
The file was modified	`thys/Berlekamp_Zassenhaus/Factor_Bound.thy` (diff)
The file was modified	`thys/Berlekamp_Zassenhaus/Mahler_Measure.thy` (diff)
The file was modified	`thys/LLL_Basis_Reduction/Norms.thy` (diff)
The file was modified	`thys/LLL_Factorization/Factor_Bound_2.thy` (diff)