Skip to content
[Jenkins]Jenkins
log in
Success

Changes

Summary

  1. delete auxiliary class comm_monoid_mult_0 and friends, and use comm_semiring_1, ... instead reason: avoid confusion of yet another definition of irreducible, prime_elem, etc. with lemma-duplication
  2. removing unused/outdated lemmas on resultants
  3. removing unused/outdated lemmas on resultants
Changeset 7809:237097cdf4b1 by rene thiemann _rene.thiemann@uibk.ac.at_:
delete auxiliary class comm_monoid_mult_0 and friends, and use comm_semiring_1, ... instead<br>reason: avoid confusion of yet another definition of irreducible, prime_elem, etc.<br>&nbsp; with lemma-duplication
The file was modified thys/Algebraic_Numbers/Algebraic_Number_Tests.thy (diff)
The file was modified thys/Algebraic_Numbers/Algebraic_Numbers.thy (diff)
The file was modified thys/Algebraic_Numbers/Algebraic_Numbers_Prelim.thy (diff)
The file was modified thys/Algebraic_Numbers/Complex_Algebraic_Numbers.thy (diff)
The file was modified thys/Algebraic_Numbers/Real_Algebraic_Numbers.thy (diff)
The file was modified thys/Algebraic_Numbers/Real_Factorization.thy (diff)
The file was modified thys/Berlekamp_Zassenhaus/Berlekamp_Zassenhaus.thy (diff)
The file was modified thys/Berlekamp_Zassenhaus/Factorize_Int_Poly.thy (diff)
The file was modified thys/Berlekamp_Zassenhaus/Unique_Factorization.thy (diff)
The file was modified thys/Berlekamp_Zassenhaus/Unique_Factorization_Poly.thy (diff)
Changeset 7808:e1570f4597b6 by rene thiemann _rene.thiemann@uibk.ac.at_:
removing unused/outdated lemmas on resultants
The file was modified thys/Algebraic_Numbers/Resultant.thy (diff)
Changeset 7807:3695998b045c by rene thiemann _rene.thiemann@uibk.ac.at_:
removing unused/outdated lemmas on resultants
The file was modified thys/Algebraic_Numbers/Resultant.thy (diff)