Mathematical Structure as Class

Mathematical structures (specially algebraic structures) can be formalized as classes in our language.
Take the most simple algebraic structure -- semigroup -- as a exmaple.
  • a set -- Element: Type,
  • a binary operation -- mul,
  • an a proof that the binary operation is associative -- mul_is_associative.
See structures/group.md for more examples.