/[mojave]/metaprl/theories/czf/czf_itt_normal_subgroup.mli
ViewVC logotype

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

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: 803 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.)

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.


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