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