Nuprl Definition : eqv_mod_subset
a ≡ b (mod s in g) == s (a * (~ b))
Definitions occuring in Statement :
grp_inv: ~,
grp_op: *,
infix_ap: x f y,
apply: f a
Definitions occuring in definition :
infix_ap: x f y,
grp_op: *,
apply: f a,
grp_inv: ~
Latex:
a \mequiv{} b (mod s in g) == s (a * (\msim{} b))
Date html generated:
2016_05_15-PM-00_09_01
Last ObjectModification:
2015_09_23-AM-06_24_24
Theory : groups_1
Home
Index