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