| changeset 2907 | 0e272e4c7cb2 |
| parent 1247 | 18b1441fb603 |
| child 8920 | af5e09b6c208 |
| 2906:171dedbc9bdb | 2907:0e272e4c7cb2 |
|---|---|
17 (* groups *) |
17 (* groups *) |
18 |
18 |
19 axclass |
19 axclass |
20 group < semigroup |
20 group < semigroup |
21 left_unit "1 <*> x = x" |
21 left_unit "1 <*> x = x" |
22 left_inv "inv x <*> x = 1" |
22 left_inverse "inverse x <*> x = 1" |
23 |
23 |
24 |
24 |
25 (* abelian groups *) |
25 (* abelian groups *) |
26 |
26 |
27 axclass |
27 axclass |