λδ digital library (LDDL)
Constant
Informal description: ""
{λ[x:complex].λ[n:{(0c).(x)}.nis].λ[o:{(0).((x).re)}.nis].λ[i:{(0).((x).im)}.is]}.<((x).mod2).pos>.{({(o).((x).re)}.possq).({({({(i).((x).im).((x).im)}.ts01).((x).im2).((x).re2)}.pl02).((x).re2).((x).mod2).(real)}.symis).((x).mod2).((x).re2)}.ispos Validation parameters: sort hierarchy = "Z2", kernel options = ""
Last update: Sat, 12 Dec 2020 10:46:54 +0100