theory C2
imports "HOL-Algebra.Group"
begin
section ‹The group C2›
text ‹
two-element group is defined over the set of boolean values. This allows to
the equality of boolean values as the group operation.
›
definition "C2"
where "C2 = ( carrier = UNIV, mult = (=), one = True )"
lemma [simp]: "(⊗) = (=)"
unfolding C2_def by simp
lemma [simp]: "1 = True"
unfolding C2_def by simp
lemma [simp]: "carrier C2 = UNIV"
unfolding C2_def by simp
lemma C2_is_group: "group C2"
unfolding C2_def
by (rule groupI, auto simp add:Units_def)
end
¤ Dauer der Verarbeitung: 0.2 Sekunden
¤
*© Formatika GbR, Deutschland
