src/HOL/Computational_Algebra/Computational_Algebra.thy
author paulson <lp15@cam.ac.uk>
Mon, 19 Feb 2024 14:12:20 +0000
changeset 79670 f471e1715fc4
parent 70817 dd675800469d
permissions -rw-r--r--
A small collection of new and useful facts, including the AM-GM inequality


section \<open>Pieces of computational Algebra\<close>

theory Computational_Algebra
imports
  Euclidean_Algorithm
  Factorial_Ring
  Formal_Laurent_Series
  Fraction_Field
  Fundamental_Theorem_Algebra
  Group_Closure
  Normalized_Fraction
  Nth_Powers
  Polynomial_FPS
  Polynomial
  Polynomial_Factorial
  Primes
  Squarefree
begin

end