Summary
- More factorization results with "irreducible"
- merge
- forgotten build
- renamed is_projection -> is_oc_projection
The file was modified | thys/Berlekamp_Zassenhaus/Berlekamp_Zassenhaus.thy (diff) |
The file was modified | thys/Berlekamp_Zassenhaus/Reconstruction.thy (diff) |
The file was modified | thys/Perron_Frobenius/Roots_Unity.thy (diff) |
The file was modified | thys/LLL_Factorization/Factorization_Algorithm_16_22.thy (diff) |
The file was modified | thys/LLL_Basis_Reduction/Gram_Schmidt_2.thy (diff) |
The file was modified | thys/LLL_Basis_Reduction/LLL.thy (diff) |