Nuprl Definition : quot_grp_car
|g//h| == a,b:|g|//a ≡ b (mod h in g)
Definitions occuring in Statement :
eqv_mod_subset: a ≡ b (mod s in g),
grp_car: |g|,
quotient: x,y:A//B[x; y]
Definitions occuring in definition :
quotient: x,y:A//B[x; y],
grp_car: |g|,
eqv_mod_subset: a ≡ b (mod s in g)
Latex:
|g//h| == a,b:|g|//a \mequiv{} b (mod h in g)
Date html generated:
2016_05_15-PM-00_09_17
Last ObjectModification:
2015_09_23-AM-06_24_27
Theory : groups_1
Home
Index