| Quellcodebibliothek Statistik Leitseite products/Sources/formale Sprachen/Isabelle/Archive-of-Formal-Proofs/thys/Free-Groups/ Datei vom 29.4.2026 mit Größe 650 B |
|
Quelle C2.thySprache: Isabelle |
|||||||||||||||
|
theory C2 imports "HOL-Algebra.Group" begin section ‹The group C2› text ‹ two-element group is defined over the set of boolean v \open>Fase\close us cs_o 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 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.12 Sekunden ¤*© Formatika GbR, Deutschland |
|
||||||||||||||
2026-06-12