HomeIsabelle/Phabricator
Diffusion afp-devel fbfac64da6d5

move parts of Min_Int_Poly from Hermite-Lindemann and Cubic_Quartic_Equations…
fbfac64da6d5
Actions

Description

move parts of Min_Int_Poly from Hermite-Lindemann and Cubic_Quartic_Equations into Algebraic_Numbers

Details

Provenance
Rene Thiemann <rene.thiemann@uibk.ac.at>Authored on
Parents
rAFP6929ff388470: ported Cubic_Quartic_Equations from AFP 2021 to devel
Branches
Unknown
Tags
Unknown

Changes (16)

PathSize
Algebraic_Numbers/
Hermite_Lindemann/
Min_Int_Poly_Complex_Impl.thy
Min_Int_Poly_Impl.thy
Polynomial_Factorization/

rAFPfbfac64da6d5

View Options

thys/Algebraic_Numbers/Min_Int_Poly.thy

Loading...
View Options

thys/Algebraic_Numbers/Real_Algebraic_Numbers.thy

Loading...
View Options

thys/Cubic_Quartic_Equations/Complex_Roots.thy

Loading...
View Options

thys/Cubic_Quartic_Equations/Cubic_Polynomials.thy

Loading...
View Options

thys/Cubic_Quartic_Equations/Min_Int_Poly_Complex_Impl.thy

Loading...
View Options

thys/Cubic_Quartic_Equations/Min_Int_Poly_Impl.thy

Loading...
View Options

thys/Cubic_Quartic_Equations/Quartic_Polynomials.thy

Loading...
View Options

thys/Cubic_Quartic_Equations/ROOT

Loading...
View Options

thys/Hermite_Lindemann/Hermite_Lindemann.thy

Loading...
View Options

thys/Hermite_Lindemann/Min_Int_Poly.thy

Loading...
View Options

thys/Hermite_Lindemann/More_Min_Int_Poly.thy

Loading...
View Options

thys/Polynomial_Factorization/Explicit_Roots.thy

Loading...