Skip to content
[Jenkins]Jenkins
log in
Failed

Changes

Summary

  1. merge
  2. new invariant in algebraic numbers: polynomials are square-free
  3. provide two formats for factorization: square-free - (f,i) encodes f^(i+1) - and normal - (f,i) ~ f^i
  4. factorization of rational polynomial delivers at least square-free factorization
  5. changed definition of square_free: 0 is NOT square_free
Changeset 6704:ddd6e4236076 by rene thiemann _rene.thiemann@uibk.ac.at_:
merge
Changeset 6703:d6a34497bd7d by rene thiemann _rene.thiemann@uibk.ac.at_:
new invariant in algebraic numbers: polynomials are square-free
The file was modified thys/Algebraic_Numbers/Algebraic_Number_Tests.thy (diff)
The file was modified thys/Algebraic_Numbers/Algebraic_Numbers_Prelim.thy (diff)
The file was modified thys/Algebraic_Numbers/Complex_Algebraic_Numbers.thy (diff)
The file was modified thys/Algebraic_Numbers/Real_Algebraic_Numbers.thy (diff)
The file was modified thys/Algebraic_Numbers/Real_Roots.thy (diff)
The file was modified thys/Algebraic_Numbers/Sturm_Rat.thy (diff)
Changeset 6702:57a940b8a3be by rene thiemann _rene.thiemann@uibk.ac.at_:
provide two formats for factorization: square-free - (f,i) encodes f^(i+1) - and normal - (f,i) ~ f^i
The file was modified thys/Polynomial_Factorization/Rational_Factorization.thy (diff)
Changeset 6701:8fac40dab1b3 by rene thiemann _rene.thiemann@uibk.ac.at_:
factorization of rational polynomial delivers at least square-free factorization
The file was modified thys/Polynomial_Factorization/Factorization_Oracle.thy (diff)
The file was modified thys/Polynomial_Factorization/Rational_Factorization.thy (diff)
The file was modified thys/Polynomial_Factorization/Square_Free_Factorization.thy (diff)
Changeset 6700:aeb856fe43df by rene thiemann _rene.thiemann@uibk.ac.at_:
changed definition of square_free: 0 is NOT square_free
The file was modified thys/Polynomial_Factorization/Factorization_Oracle.thy (diff)
The file was modified thys/Polynomial_Factorization/Rational_Factorization.thy (diff)
The file was modified thys/Polynomial_Factorization/Square_Free_Factorization.thy (diff)