Nuprl Definition : mk-s-group
mk-s-group(ss; e; i; o; sep; invsep) == ss["id" := e]["inv" := i]["op" := o]["opsep" := sep]["invsep" := invsep]
Definitions occuring in Statement :
token: "$token",
record-update: r[x := v]
Definitions occuring in definition :
record-update: r[x := v],
token: "$token"
Latex:
mk-s-group(ss; e; i; o; sep; invsep) ==
ss["id" := e]["inv" := i]["op" := o]["opsep" := sep]["invsep" := invsep]
Date html generated:
2019_10_31-AM-07_27_44
Last ObjectModification:
2019_09_19-PM-04_28_54
Theory : constructive!algebra
Home
Index