Changes

Summary

merge
Adapted Deep_Learning for changes in Jordan_Normal_Form
Improved locale interpretations
Generalized abstract conjugate
merge
merged
Various generalizations and cleanings

Changeset 8101:d3d1dcee1acc by akihisayamada _akihisa.yamada@uibk.ac.at_: merge
Changeset 8100:eb0d9efc948f by akihisayamada _akihisa.yamada@uibk.ac.at_: Adapted Deep_Learning for changes in Jordan_Normal_Form
The file was modified	`thys/Deep_Learning/DL_Missing_VS_Connect.thy` (diff)
The file was modified	`thys/Deep_Learning/DL_Rank.thy` (diff)
The file was modified	`thys/Deep_Learning/DL_Rank_Submatrix.thy` (diff)
Changeset 8099:5290ed572816 by akihisayamada _akihisa.yamada@uibk.ac.at_: Improved locale interpretations
The file was modified	`thys/Berlekamp_Zassenhaus/Berlekamp_Type_Based.thy` (diff)
The file was modified	`thys/Jordan_Normal_Form/Conjugate.thy` (diff)
The file was modified	`thys/Jordan_Normal_Form/Gram_Schmidt.thy` (diff)
The file was modified	`thys/Jordan_Normal_Form/Matrix_Kernel.thy` (diff)
The file was modified	`thys/Jordan_Normal_Form/VS_Connect.thy` (diff)
Changeset 8098:26ebf60d8ffe by akihisayamada _akihisa.yamada@uibk.ac.at_: Generalized abstract conjugate
The file was modified	`thys/Jordan_Normal_Form/Conjugate.thy` (diff)
Changeset 8097:c3b3f2051d4f by akihisayamada _akihisa.yamada@uibk.ac.at_: merge
Changeset 8096:fb41d6bdd2ea by akihisayamada _akihisa.yamada@uibk.ac.at_: merged
Changeset 8095:75c0955e5e44 by akihisayamada _akihisa.yamada@uibk.ac.at_: Various generalizations and cleanings
The file was modified	`thys/Algebraic_Numbers/Algebraic_Numbers.thy` (diff)
The file was modified	`thys/Algebraic_Numbers/Algebraic_Numbers_Prelim.thy` (diff)
The file was modified	`thys/Algebraic_Numbers/Complex_Algebraic_Numbers.thy` (diff)
The file was modified	`thys/Algebraic_Numbers/Complex_Roots_Real_Poly.thy` (diff)
The file was modified	`thys/Algebraic_Numbers/Real_Algebraic_Numbers.thy` (diff)
The file was modified	`thys/Algebraic_Numbers/Real_Factorization.thy` (diff)
The file was modified	`thys/Algebraic_Numbers/Real_Roots.thy` (diff)
The file was modified	`thys/Algebraic_Numbers/Show_Real_Precise.thy` (diff)
The file was modified	`thys/Algebraic_Numbers/Sturm_Rat.thy` (diff)
The file was modified	`thys/Berlekamp_Zassenhaus/Berlekamp_Type_Based.thy` (diff)
The file was modified	`thys/Berlekamp_Zassenhaus/Bivariate_Polynomials.thy` (diff)
The file was modified	`thys/Berlekamp_Zassenhaus/Factor_Bound.thy` (diff)
The file was modified	`thys/Berlekamp_Zassenhaus/Factorize_Rat_Poly.thy` (diff)
The file was modified	`thys/Berlekamp_Zassenhaus/Finite_Field.thy` (diff)
The file was modified	`thys/Berlekamp_Zassenhaus/Finite_Field_Factorization_Record_Based.thy` (diff)
The file was modified	`thys/Berlekamp_Zassenhaus/Finite_Field_Record_Based.thy` (diff)
The file was modified	`thys/Berlekamp_Zassenhaus/Hensel_Lifting.thy` (diff)
The file was modified	`thys/Berlekamp_Zassenhaus/Hensel_Lifting_Type_Based.thy` (diff)
The file was modified	`thys/Berlekamp_Zassenhaus/Mahler_Measure.thy` (diff)
The file was modified	`thys/Berlekamp_Zassenhaus/Poly_Mod.thy` (diff)
The file was modified	`thys/Berlekamp_Zassenhaus/Poly_Mod_Finite_Field.thy` (diff)
The file was modified	`thys/Berlekamp_Zassenhaus/Poly_Mod_Finite_Field_Record_Based.thy` (diff)
The file was modified	`thys/Berlekamp_Zassenhaus/Resultant.thy` (diff)
The file was modified	`thys/Berlekamp_Zassenhaus/Square_Free_Factorization_Int.thy` (diff)
The file was modified	`thys/Berlekamp_Zassenhaus/Square_Free_Int_To_Square_Free_GFp.thy` (diff)
The file was modified	`thys/Berlekamp_Zassenhaus/Suitable_Prime.thy` (diff)
The file was modified	`thys/Berlekamp_Zassenhaus/Unique_Factorization.thy` (diff)
The file was modified	`thys/Berlekamp_Zassenhaus/Unique_Factorization_Poly.thy` (diff)
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/Matrix.thy` (diff)
The file was modified	`thys/Polynomial_Factorization/Dvd_Int_Poly.thy` (diff)
The file was modified	`thys/Polynomial_Factorization/Gauss_Lemma.thy` (diff)
The file was modified	`thys/Polynomial_Factorization/Gcd_Rat_Poly.thy` (diff)
The file was modified	`thys/Polynomial_Factorization/Kronecker_Factorization.thy` (diff)
The file was modified	`thys/Polynomial_Factorization/Square_Free_Factorization.thy` (diff)
The file was modified	`thys/Polynomial_Interpolation/Newton_Interpolation.thy` (diff)
The file was modified	`thys/Polynomial_Interpolation/Polynomial_Interpolation.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 modified	`thys/Subresultants/Subresultant.thy` (diff)
The file was modified	`thys/Subresultants/Subresultant_Gcd.thy` (diff)