Nuprl Definition : gcopower_sig
gcopower_sig{i:l}(s;g) == grp:GrpSig × inj:|s| ⟶ |g| ⟶ |grp| × (h:AbGrp ⟶ (|s| ⟶ |g| ⟶ |h|) ⟶ |grp| ⟶ |h|)
Definitions occuring in Statement :
function: x:A ⟶ B[x],
product: x:A × B[x],
abgrp: AbGrp,
grp_car: |g|,
grp_sig: GrpSig,
set_car: |p|
Definitions occuring in definition :
grp_sig: GrpSig,
product: x:A × B[x],
abgrp: AbGrp,
set_car: |p|,
function: x:A ⟶ B[x],
grp_car: |g|
FDL editor aliases :
gcopower_sig
Latex:
gcopower\_sig\{i:l\}(s;g) ==
grp:GrpSig \mtimes{} inj:|s| {}\mrightarrow{} |g| {}\mrightarrow{} |grp| \mtimes{} (h:AbGrp {}\mrightarrow{} (|s| {}\mrightarrow{} |g| {}\mrightarrow{} |h|) {}\mrightarrow{} |grp| {}\mrightarrow{} |h|)
Date html generated:
2016_05_16-AM-08_13_36
Last ObjectModification:
2015_09_23-AM-09_52_32
Theory : polynom_1
Home
Index