This symbol is a constructor for groups. It takes four arguments in
the following order: a set to specify the elements in the group, a
binary operation to specify the group operation, an element to specify the
identity, and a unary operation to
specify inverses of group elements. Both the binary and unary operations should act on elements
of the set and return an element of the set.
Commented Mathematical property (CMP):
A group is closed under its operation.
A groups operation is associative.
A group has an identity element.
Every element of a group has an inverse.
implies
(eq
( G, group
( set, binop, elt, unop)
)
, and
(implies
(and
(in
( x, set)
, in
( y, set)
)
, in
( binop
( x, y)
, set)
)
, eq
( binop
( x, binop
( y, z)
)
, binop
( binop
( x, y)
, z)
)
, and
(in
( elt, set)
, forall
[
x
] .
(implies
(in
( x, set)
, and
(eq
( binop
( elt, x)
, x)
, eq
( binop
( x, elt)
, x)
)
)
)
)
, forall
[
x
] .
(implies
(in
( x, set)
, eq
( binop
( x, unop
( x)
)
, elt)
)
)
)
)
$G = group1.group($set, $binop, $elt, $unop) ==> (set1.in($x, $set) and set1.in($y, $set) ==> set1.in($binop($x, $y), $set)) and $binop($x, $binop($y, $z)) = $binop($binop($x, $y), $z) and set1.in($elt, $set) and quant1.forall[$x -> set1.in($x, $set) ==> $binop($elt, $x) = $x and $binop($x, $elt) = $x] and quant1.forall[$x -> set1.in($x, $set) ==> $binop($x, $unop($x)) = $elt]
Example:
This example represents the group which has as elements all positive
and negative even numbers, the group operation is binary addition,
inverses are the negative of the element and the identity is the zero
element.
This symbol represents a unary function, whose argument should be a
group G (for instance constructed by group).
When applied to G, its value should be the set of elements of G.
This symbol is a constructor symbol with one or two arguments. The
first argument is a list or set, D, of group elements. The optional
second argument is the group G containing D. It denotes the subgroup
of G generated by D.
This is a symbol with three arguments.
The first argument is a group G. Its second argument
is an element g of G and the third argument is
an integer k.
It denotes the element g^k in G.
This symbol is a function with two arguments. Its first
argument should be a group. The
second should be an arithmetic expression A,
whose operators are
times and power, and whose leaves are members of the carrier of G.
When applied to
G and A, it denotes the element (of G) that is obtained from the
leaves of A by applying the multiplication and the power map of G instead of the
times and power
from the CD arith1 appearing in A.
The symbol alg1.one occurring in A will be interpreted as
the identity of G.
The binary function whose value is the set of conjugates of
the elements of the second group by elements of the first,
where multiplication between them is defined.
Commented Mathematical property (CMP):
n in the normal closure (A,B) implies
there exists a in A and b in B s.t. n = b^(-1) a b
If G, H are the group arguments, then IsNormal(G,H) returns true precisely when
H is normal in G. That is, inverse(g)*h*g is defined and contained in H for
all h in H and g in G.
Commented Mathematical property (CMP):
is_normal(G,H) implies that for all g in G and h in H then
inverse(g)*h*g is in H.