--- a/src/HOL/Computational_Algebra/Factorial_Ring.thy Mon Oct 18 18:33:46 2021 +0200
+++ b/src/HOL/Computational_Algebra/Factorial_Ring.thy Fri Oct 15 18:09:34 2021 +0200
@@ -313,7 +313,7 @@
context
begin
-private lemma prime_elem_powerD:
+lemma prime_elem_powerD:
assumes "prime_elem (p ^ n)"
shows "prime_elem p \<and> n = 1"
proof (cases n)
--- a/src/HOL/Computational_Algebra/Polynomial_Factorial.thy Mon Oct 18 18:33:46 2021 +0200
+++ b/src/HOL/Computational_Algebra/Polynomial_Factorial.thy Fri Oct 15 18:09:34 2021 +0200
@@ -525,7 +525,7 @@
qed
qed
-private lemma irreducible_imp_prime_poly:
+lemma irreducible_imp_prime_poly:
fixes p :: "'a :: {factorial_semiring,semiring_Gcd,ring_gcd,idom_divide,semiring_gcd_mult_normalize} poly"
assumes "irreducible p"
shows "prime_elem p"
@@ -615,7 +615,7 @@
subsection \<open>Prime factorisation of polynomials\<close>
-private lemma poly_prime_factorization_exists_content_1:
+lemma poly_prime_factorization_exists_content_1:
fixes p :: "'a :: {factorial_semiring,semiring_Gcd,ring_gcd,idom_divide,semiring_gcd_mult_normalize} poly"
assumes "p \<noteq> 0" "content p = 1"
shows "\<exists>A. (\<forall>p. p \<in># A \<longrightarrow> prime_elem p) \<and> prod_mset A = normalize p"