Summary
- index_times_mat -> index_mult_mat, more lemmas on binary minus for vectors and matrices
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/Schur_Decomposition.thy (diff) |
The file was modified | thys/Subresultants/Subresultant.thy (diff) |