Nuprl Definition : fma_from_gcp
fma_from_gcp(g;r;c;a) == <a, λp:|g|. c.inj p 1, λa.(λh:|g| ⟶ a.car. c.umap (a↓grp) (λp:|g|. λv:|r|. a.act v (h p)))>
Definitions occuring in Statement :
gcopower_umap: g1.umap,
gcopower_inj: g1.inj,
grp_of_module: m↓grp,
alg_act: a.act,
alg_car: a.car,
tlambda: λx:T. b[x],
apply: f a,
lambda: λx.A[x],
function: x:A ⟶ B[x],
pair: <a, b>,
rng_one: 1,
rng_car: |r|,
grp_car: |g|
Definitions occuring in definition :
pair: <a, b>,
gcopower_inj: g1.inj,
rng_one: 1,
lambda: λx.A[x],
function: x:A ⟶ B[x],
alg_car: a.car,
gcopower_umap: g1.umap,
grp_of_module: m↓grp,
grp_car: |g|,
tlambda: λx:T. b[x],
rng_car: |r|,
alg_act: a.act,
apply: f a
Latex:
fma\_from\_gcp(g;r;c;a) ==
<a, \mlambda{}p:|g|. c.inj p 1, \mlambda{}a.(\mlambda{}h:|g| {}\mrightarrow{} a.car. c.umap (a\mdownarrow{}grp) (\mlambda{}p:|g|. \mlambda{}v:|r|. a.act v (h p)))>
Date html generated:
2016_05_16-AM-08_14_47
Last ObjectModification:
2015_09_23-AM-09_52_47
Theory : polynom_1
Home
Index