Skip to content
Jenkins
log in
Dashboard
Thibault Dardinier <thibault.dardinier@inf.ethz.ch>
My Views
All
afp-repo
#227
Changes
Status
Changes
Console Output
View Build Information
Polling Log
Environment Variables
Mercurial Build Data
Embeddable Build Status
Previous Build
Next Build
Failed
Changes
Summary
merge
moved lemmas
improved code-equation for poly_inverse
invariant of algebraic number implementation: polynomials are square-free
factorize_rat_poly delivers square-free poly, independent of oracle
Changeset
6698:f7b132c3c792
by
rene thiemann _rene.thiemann@uibk.ac.at_
:
merge
Changeset
6697:fab59516109e
by
rene thiemann _rene.thiemann@uibk.ac.at_
:
moved lemmas
The file was added
thys/Polynomial_Factorization/Fundamental_Theorem_Algebra_Factorized.thy
The file was modified
thys/Algebraic_Numbers/Algebraic_Numbers_Prelim.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/Deriving/Comparator_Generator/Compare_Real.thy
(diff)
The file was modified
thys/Jordan_Normal_Form/Char_Poly.thy
(diff)
The file was modified
thys/Polynomial_Factorization/Square_Free_Factorization.thy
(diff)
The file was modified
thys/Polynomial_Interpolation/Missing_Polynomial.thy
(diff)
Changeset
6696:8c3e2c0bdbb3
by
rene thiemann _rene.thiemann@uibk.ac.at_
:
improved code-equation for poly_inverse
The file was modified
thys/Algebraic_Numbers/Algebraic_Numbers_Prelim.thy
(diff)
Changeset
6695:0489cb882df1
by
rene thiemann _rene.thiemann@uibk.ac.at_
:
invariant of algebraic number implementation: polynomials are square-free
The file was modified
thys/Algebraic_Numbers/Algebraic_Numbers_Prelim.thy
(diff)
The file was modified
thys/Algebraic_Numbers/Real_Algebraic_Numbers.thy
(diff)
Changeset
6694:9c4e440fa256
by
rene thiemann _rene.thiemann@uibk.ac.at_
:
factorize_rat_poly delivers square-free poly, independent of oracle
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)