Skip to content
[Jenkins]Jenkins
log in
Success

Changes

Summary

  1. Lifting UFD properties into Poly_Mod.
Changeset 8290:e4fe240b333f by akihisayamada _akihisa.yamada@uibk.ac.at_:
Lifting UFD properties into Poly_Mod.
The file was addedthys/Berlekamp_Zassenhaus/Missing_Multiset2.thy
The file was addedthys/Berlekamp_Zassenhaus/Unique_Factorization.thy
The file was addedthys/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 removedthys/Algebraic_Numbers/Unique_Factorization.thy
The file was removedthys/Algebraic_Numbers/Unique_Factorization_Poly.thy