Summary
- invoke normalization of polynomials before invoking poly_add and poly_mult => one can compute resultants of integer polynomials instead of rational polynomials
The file was modified | thys/Algebraic_Numbers/Real_Algebraic_Numbers.thy (diff) |
The file was modified | thys/Algebraic_Numbers/Real_Algebraic_Numbers.thy (diff) |