Nuprl Lemma : one-dim-int-vs
one-dim-vs(ℤ-rng) ~ ℤ
Proof
Definitions occuring in Statement :
int-vs: ℤ,
one-dim-vs: one-dim-vs(K),
sqequal: s ~ t,
int_ring: ℤ-rng
Definitions unfolded in proof :
int-vs: ℤ,
int_ring: ℤ-rng,
one-dim-vs: one-dim-vs(K),
rng_car: |r|,
pi1: fst(t),
rng_zero: 0,
pi2: snd(t),
rng_plus: +r,
rng_times: *,
infix_ap: x f y
Rules used in proof :
sqequalSubstitution,
sqequalTransitivity,
computationStep,
sqequalReflexivity,
sqequalRule
Latex:
one-dim-vs(\mBbbZ{}-rng) \msim{} \mBbbZ{}
Date html generated:
2019_10_31-AM-06_26_41
Last ObjectModification:
2019_08_02-PM-03_57_39
Theory : linear!algebra
Home
Index