Summary
- avoid import of Multivariate_Analysis/Multivariate_Analysis to avoid Product_Order
The file was modified | thys/Cayley_Hamilton/Square_Matrix.thy (diff) |
The file was modified | thys/Perron_Frobenius/Perron_Frobenius.thy (diff) |
The file was modified | thys/Rank_Nullity_Theorem/Fundamental_Subspaces.thy (diff) |
The file was modified | thys/Rank_Nullity_Theorem/Generalizations.thy (diff) |