Changes

Summary

merge
restructured matrix-library to use syntactic +,-,... classes, more uniform lemma-names

Changeset 8238:49fe0f75ded7 by rene thiemann _rene.thiemann@uibk.ac.at_: merge
Changeset 8237:b6b0c1b49d0e by rene thiemann _rene.thiemann@uibk.ac.at_: restructured matrix-library to use syntactic +,-,... classes, more uniform lemma-names
The file was modified	`thys/Algebraic_Numbers/Resultant.thy` (diff)
The file was modified	`thys/Berlekamp_Zassenhaus/Berlekamp_Type_Based.thy` (diff)
The file was modified	`thys/Berlekamp_Zassenhaus/Finite_Field_Factorization_Record_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_Deep_Model_Poly.thy` (diff)
The file was modified	`thys/Deep_Learning/DL_Flatten_Matrix.thy` (diff)
The file was modified	`thys/Deep_Learning/DL_Fundamental_Theorem_Network_Capacity.thy` (diff)
The file was modified	`thys/Deep_Learning/DL_Missing_Matrix.thy` (diff)
The file was modified	`thys/Deep_Learning/DL_Missing_VS_Connect.thy` (diff)
The file was modified	`thys/Deep_Learning/DL_Network.thy` (diff)
The file was modified	`thys/Deep_Learning/DL_Rank.thy` (diff)
The file was modified	`thys/Deep_Learning/DL_Rank_CP_Rank.thy` (diff)
The file was modified	`thys/Deep_Learning/DL_Rank_Submatrix.thy` (diff)
The file was modified	`thys/Deep_Learning/DL_Shallow_Model.thy` (diff)
The file was modified	`thys/Deep_Learning/DL_Submatrix.thy` (diff)
The file was modified	`thys/Deep_Learning/Tensor_Matricization.thy` (diff)
The file was modified	`thys/Jordan_Normal_Form/Char_Poly.thy` (diff)
The file was modified	`thys/Jordan_Normal_Form/Column_Operations.thy` (diff)
The file was modified	`thys/Jordan_Normal_Form/Determinant.thy` (diff)
The file was modified	`thys/Jordan_Normal_Form/Determinant_Impl.thy` (diff)
The file was modified	`thys/Jordan_Normal_Form/Gauss_Jordan_Elimination.thy` (diff)
The file was modified	`thys/Jordan_Normal_Form/Gauss_Jordan_IArray_Impl.thy` (diff)
The file was modified	`thys/Jordan_Normal_Form/Gram_Schmidt.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/Jordan_Normal_Form_Uniqueness.thy` (diff)
The file was modified	`thys/Jordan_Normal_Form/Matrix.thy` (diff)
The file was modified	`thys/Jordan_Normal_Form/Matrix_Comparison.thy` (diff)
The file was modified	`thys/Jordan_Normal_Form/Matrix_Complexity.thy` (diff)
The file was modified	`thys/Jordan_Normal_Form/Matrix_IArray_Impl.thy` (diff)
The file was modified	`thys/Jordan_Normal_Form/Matrix_Impl.thy` (diff)
The file was modified	`thys/Jordan_Normal_Form/Matrix_Kernel.thy` (diff)
The file was modified	`thys/Jordan_Normal_Form/Ring_Hom_Matrix.thy` (diff)
The file was modified	`thys/Jordan_Normal_Form/Schur_Decomposition.thy` (diff)
The file was modified	`thys/Jordan_Normal_Form/Spectral_Radius.thy` (diff)
The file was modified	`thys/Jordan_Normal_Form/Strassen_Algorithm.thy` (diff)
The file was modified	`thys/Jordan_Normal_Form/Strassen_Algorithm_Code.thy` (diff)
The file was modified	`thys/Jordan_Normal_Form/VS_Connect.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/Spectral_Radius_Theory.thy` (diff)
The file was modified	`thys/Subresultants/Resultant_Prelim.thy` (diff)
The file was modified	`thys/Subresultants/Subresultant.thy` (diff)