Nuprl Definition : mdivides
b | a == ∃c:|g|. (a = (b * c) ∈ |g|)
Definitions occuring in Statement :
infix_ap: x f y,
exists: ∃x:A. B[x],
equal: s = t ∈ T,
grp_op: *,
grp_car: |g|
Definitions occuring in definition :
exists: ∃x:A. B[x],
equal: s = t ∈ T,
grp_car: |g|,
infix_ap: x f y,
grp_op: *
Latex:
b | a == \mexists{}c:|g|. (a = (b * c))
Date html generated:
2016_05_16-AM-07_42_51
Last ObjectModification:
2015_09_23-AM-09_51_50
Theory : factor_1
Home
Index