Summary
- improved equality test of algebraic numbers by using new irreducible-invariant
- use invariant that polynomial of algebraic number representation is irreducible, exploit this in algorithms
The file was modified | thys/Algebraic_Numbers/Real_Algebraic_Numbers.thy (diff) |
The file was modified | thys/Algebraic_Numbers/Algebraic_Number_Tests.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/Show_Real_Precise.thy (diff) |