--- a/src/HOL/Groups_List.thy Fri May 02 17:24:43 2025 +0200
+++ b/src/HOL/Groups_List.thy Sun May 04 12:18:27 2025 +0100
@@ -665,4 +665,7 @@
"prod_list xs = 0 \<longleftrightarrow> (0 :: 'a :: {semiring_no_zero_divisors, semiring_1}) \<in> set xs"
by (induction xs) simp_all
+lemma prod_list_nonneg: "(\<And> x. (x :: 'a :: ordered_semiring_1) \<in> set xs \<Longrightarrow> x \<ge> 0) \<Longrightarrow> prod_list xs \<ge> 0"
+ by (induct xs) auto
+
end
--- a/src/HOL/Rings.thy Fri May 02 17:24:43 2025 +0200
+++ b/src/HOL/Rings.thy Sun May 04 12:18:27 2025 +0100
@@ -1987,6 +1987,8 @@
subclass ordered_semiring_0 ..
+subclass ordered_cancel_ab_semigroup_add ..
+
end
class linordered_semiring = ordered_semiring + linordered_cancel_ab_semigroup_add