Nuprl Definition : ringeq_int_terms
t1 ≡ t2 == ∀f:ℤ ⟶ |r|. (ring_term_value(f;t1) = ring_term_value(f;t2) ∈ |r|)
Definitions occuring in Statement :
ring_term_value: ring_term_value(f;t),
rng_car: |r|,
all: ∀x:A. B[x],
function: x:A ⟶ B[x],
int: ℤ,
equal: s = t ∈ T
Definitions occuring in definition :
all: ∀x:A. B[x],
function: x:A ⟶ B[x],
int: ℤ,
equal: s = t ∈ T,
rng_car: |r|,
ring_term_value: ring_term_value(f;t)
FDL editor aliases :
ringeq_int_terms
Latex:
t1 \mequiv{} t2 == \mforall{}f:\mBbbZ{} {}\mrightarrow{} |r|. (ring\_term\_value(f;t1) = ring\_term\_value(f;t2))
Date html generated:
2018_05_21-PM-03_15_47
Last ObjectModification:
2018_01_25-AM-11_19_46
Theory : rings_1
Home
Index