Nuprl Definition : integ_dom_p
IsIntegDom(r) == 0 ≠ 1 ∈ |r| ∧ (∀u,v:|r|. ((¬(v = 0 ∈ |r|)) ⇒ ((u * v) = 0 ∈ |r|) ⇒ (u = 0 ∈ |r|)))
Definitions occuring in Statement :
rng_one: 1,
rng_times: *,
rng_zero: 0,
rng_car: |r|,
infix_ap: x f y,
all: ∀x:A. B[x],
nequal: a ≠ b ∈ T ,
not: ¬A,
implies: P ⇒ Q,
and: P ∧ Q,
equal: s = t ∈ T
Definitions occuring in definition :
and: P ∧ Q,
nequal: a ≠ b ∈ T ,
rng_one: 1,
all: ∀x:A. B[x],
not: ¬A,
implies: P ⇒ Q,
infix_ap: x f y,
rng_times: *,
equal: s = t ∈ T,
rng_car: |r|,
rng_zero: 0
Latex:
IsIntegDom(r) == 0 \mneq{} 1 \mmember{} |r| \mwedge{} (\mforall{}u,v:|r|. ((\mneg{}(v = 0)) {}\mRightarrow{} ((u * v) = 0) {}\mRightarrow{} (u = 0)))
Date html generated:
2016_05_15-PM-00_22_22
Last ObjectModification:
2015_09_23-AM-06_25_39
Theory : rings_1
Home
Index