src/HOL/Number_Theory/Residues.thy
changeset 58889 5b7a9633cfa8
parent 57514 bdc2c6b40bf2
child 59667 651ea265d568
equal deleted inserted replaced
58888:9537bf1c4853 58889:5b7a9633cfa8
     3 
     3 
     4 An algebraic treatment of residue rings, and resulting proofs of
     4 An algebraic treatment of residue rings, and resulting proofs of
     5 Euler's theorem and Wilson's theorem.
     5 Euler's theorem and Wilson's theorem.
     6 *)
     6 *)
     7 
     7 
     8 header {* Residue rings *}
     8 section {* Residue rings *}
     9 
     9 
    10 theory Residues
    10 theory Residues
    11 imports
    11 imports
    12   UniqueFactorization
    12   UniqueFactorization
    13   Binomial
    13   Binomial