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)