Commit 5c21ce46 authored by haftmann's avatar haftmann
Browse files

subclass relation

parent c81dd066bd29
......@@ -607,9 +607,6 @@ lemma sum_indicator_eq_card2:
using sum_mult_indicator [OF assms, of "\<lambda>y. 1::nat" P "\<lambda>y. x"]
unfolding card_eq_sum by auto
subclass (in zero_less_one) zero_neq_one
by standard (use zero_less_one in blast)
lemma disjoint_family_indicator_le_1:
assumes "disjoint_family_on A I"
shows "(\<Sum> i\<in> I. indicator (A i) x) \<le> (1::'a:: {comm_monoid_add,zero_less_one})"
......@@ -29,9 +29,6 @@ hide_const(open) module.smult up_ring.monom up_ring.coeff
(**** Could be merged to HOL/Rings.thy ****)
lemma (in zero_less_one) zero_le_one [simp]: "0 \<le> 1" by (rule less_imp_le, simp)
subclass (in zero_less_one) zero_neq_one by (unfold_locales, simp add: less_imp_neq)
class ordered_semiring_1 = Rings.ordered_semiring_0 + monoid_mult + zero_less_one
Markdown is supported
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment