(* 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