ViewVC logotype

Log of /metaprl/theories/czf/czf_itt_normal_subgroup.ml

Parent Directory Parent Directory | Revision Log Revision Log

Links to HEAD: (view) (download) (annotate)
Sticky Revision:

Revision 3572 - (view) (download) (annotate) - [select for diffs]
Added Tue Apr 9 06:01:29 2002 UTC (19 years, 2 months ago) by xiny
File length: 2822 byte(s)
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.)

  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

This form allows you to request diffs between any two revisions of this file. For each of the two "sides" of the diff, enter a numeric revision.

  Diffs between and
  Type of Diff should be a

  ViewVC Help
Powered by ViewVC 1.1.26