Skip to content

Instantly share code, notes, and snippets.

@tangentstorm

tangentstorm/MJWGroups.thy

Created June 30, 2018 21:36
Show Gist options
  • Save tangentstorm/fc5aa7e3e22d595dcdfcfb5abdc30d4c to your computer and use it in GitHub Desktop.
Save tangentstorm/fc5aa7e3e22d595dcdfcfb5abdc30d4c to your computer and use it in GitHub Desktop.
Download ZIP
Raw
MJWGroups.thy
(* 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