Summary
- Lifting UFD properties into Poly_Mod.
The file was added | thys/Berlekamp_Zassenhaus/Missing_Multiset2.thy |
The file was added | thys/Berlekamp_Zassenhaus/Unique_Factorization.thy |
The file was added | thys/Berlekamp_Zassenhaus/Unique_Factorization_Poly.thy |
The file was modified | thys/Berlekamp_Zassenhaus/Berlekamp_Type_Based.thy (diff) |
The file was modified | thys/Berlekamp_Zassenhaus/Factor_Bound.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 removed | thys/Algebraic_Numbers/Unique_Factorization.thy |
The file was removed | thys/Algebraic_Numbers/Unique_Factorization_Poly.thy |