Skip to content

Instantly share code, notes, and snippets.

Embed
What would you like to do?
(* Simple Group Theory from Scratch *)
theory MJWGroups
imports Pure
begin
locale group =
fixes op :: "'g ⇒ 'g ⇒ 'g" (infixl "∘" 65)
fixes id :: "'g" ("𝔦")
fixes inv :: "'g ⇒ 'g"
assumes assoc: "(a ∘ b) ∘ c == a ∘ (b ∘ c)"
and ident: "a ∘ 𝔦 == a"
and t1: "((a=b) ∧ (c=d)) = ((a ∘ b) = (c ∘ d))"
end
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
You can’t perform that action at this time.