src/HOL/Computational_Algebra/Computational_Algebra.thy
author wenzelm
Wed Nov 01 20:46:23 2017 +0100 (22 months ago)
changeset 66983 df83b66f1d94
parent 66805 274b4edca859
child 67165 22a5822f52f7
permissions -rw-r--r--
proper merge (amending fb46c031c841);
haftmann@65417
     1
haftmann@65417
     2
section \<open>Pieces of computational Algebra\<close>
haftmann@65417
     3
haftmann@65417
     4
theory Computational_Algebra
haftmann@65417
     5
imports
haftmann@65417
     6
  Euclidean_Algorithm
haftmann@65417
     7
  Factorial_Ring
haftmann@65417
     8
  Formal_Power_Series
haftmann@65417
     9
  Fraction_Field
haftmann@65417
    10
  Fundamental_Theorem_Algebra
haftmann@65417
    11
  Normalized_Fraction
eberlm@66276
    12
  Nth_Powers
haftmann@65417
    13
  Polynomial_FPS
haftmann@65417
    14
  Polynomial
haftmann@66805
    15
  Polynomial_Factorial
haftmann@65417
    16
  Primes
eberlm@66276
    17
  Squarefree
haftmann@65417
    18
begin
haftmann@65417
    19
haftmann@65417
    20
end
haftmann@65417
    21