Nuprl Definition : mul_mon_of_rng
r↓xmn == <|r|, =b, ≤b, *, 1, λz.z>
Definitions occuring in Statement :
rng_one: 1,
rng_times: *,
rng_le: ≤b,
rng_eq: =b,
rng_car: |r|,
lambda: λx.A[x],
pair: <a, b>
Definitions occuring in definition :
rng_car: |r|,
rng_eq: =b,
rng_le: ≤b,
rng_times: *,
pair: <a, b>,
rng_one: 1,
lambda: λx.A[x]
Latex:
r\mdownarrow{}xmn == <|r|, =\msubb{}, \mleq{}\msubb{}, *, 1, \mlambda{}z.z>
Date html generated:
2016_05_15-PM-00_20_59
Last ObjectModification:
2015_09_23-AM-06_25_35
Theory : rings_1
Home
Index