Changes by: Xin Yu (xiny at cs.caltech.edu)
Date: 2002-04-08 23:01:29 -0700 (Mon, 08 Apr 2002)
Revision: 3572
Log message:
Defined normal subgroups:
A subgroup H of a group G is normal if its left and right cosets
coincide, that is, if gH = Ha for all g in G.
All subgroups of abelian groups are normal.
The kernel of a homomorphism f: G1 -> G2 is a normal subgroup of G1.
(This is proved in Czf_itt_hom.)
Note/TODO:
There is a standared way to show that two sets are equal;
show that each is a subset of the other.
I fould this method very useful and wrote it up as a tactic
"equalSubsetT", but I cannot prove it. It is better put in
Czf_itt_subset.