Nuprl Definition : formal-sum
formal-sum(K;S) ==  a,b:basic-formal-sum(K;S)//bfs-equiv(K;S;a;b)
Definitions occuring in Statement : 
bfs-equiv: bfs-equiv(K;S;fs1;fs2)
, 
basic-formal-sum: basic-formal-sum(K;S)
, 
quotient: x,y:A//B[x; y]
Definitions occuring in definition : 
quotient: x,y:A//B[x; y]
, 
basic-formal-sum: basic-formal-sum(K;S)
, 
bfs-equiv: bfs-equiv(K;S;fs1;fs2)
FDL editor aliases : 
formal-sum
Latex:
formal-sum(K;S)  ==    a,b:basic-formal-sum(K;S)//bfs-equiv(K;S;a;b)
Date html generated:
2018_05_22-PM-09_45_14
Last ObjectModification:
2017_11_10-PM-06_04_20
Theory : linear!algebra
Home
Index